Mathlib.Order.Basic

LE.le.ge theorem

[LE α] {x y : α} (h : x ≤ y) : y ≥ x

Full source

protected lemma LE.le.ge [LE α] {x y : α} (h : x ≤ y) : y ≥ x := h

Inequality Reversal: $x \leq y$ implies $y \geq x$

Informal description

For any two elements $x$ and $y$ in a type $\alpha$ equipped with a less-than-or-equal relation $\leq$, if $x \leq y$ then $y \geq x$.

GE.ge.le theorem

[LE α] {x y : α} (h : x ≥ y) : y ≤ x

Full source

protected lemma GE.ge.le [LE α] {x y : α} (h : x ≥ y) : y ≤ x := h

Equivalence of Greater-Than-Or-Equal and Less-Than-Or-Equal Relations

Informal description

For any two elements $x$ and $y$ in a type $\alpha$ equipped with a less-than-or-equal relation $\leq$, if $x \geq y$ then $y \leq x$.

LT.lt.gt theorem

[LT α] {x y : α} (h : x < y) : y > x

Full source

protected lemma LT.lt.gt [LT α] {x y : α} (h : x < y) : y > x := h

Strict Order Duality: $x < y$ implies $y > x$

Informal description

For any type $\alpha$ with a strict order relation $<$, and for any elements $x, y \in \alpha$, if $x < y$ then $y > x$.

GT.gt.lt theorem

[LT α] {x y : α} (h : x > y) : y < x

Full source

protected lemma GT.gt.lt [LT α] {x y : α} (h : x > y) : y < x := h

Strict Order Duality: $x > y$ implies $y < x$

Informal description

For any type $\alpha$ with a strict order relation $<$, and for any elements $x, y \in \alpha$, if $x > y$ then $y < x$.

Order.Preimage definition

(f : α → β) (s : β → β → Prop) (x y : α) : Prop

Full source

/-- Given a relation `R` on `β` and a function `f : α → β`, the preimage relation on `α` is defined
by `x ≤ y ↔ f x ≤ f y`. It is the unique relation on `α` making `f` a `RelEmbedding` (assuming `f`
is injective). -/
@[simp]
def Order.Preimage (f : α → β) (s : β → β → Prop) (x y : α) : Prop := s (f x) (f y)

Preimage of an order relation

Informal description

Given a relation $R$ on a type $\beta$ and a function $f : \alpha \to \beta$, the preimage relation on $\alpha$ is defined by $x \leq y \leftrightarrow f(x) \leq f(y)$. This is the unique relation on $\alpha$ that makes $f$ a relation embedding (assuming $f$ is injective).

term_⁻¹'o_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixl:80 " ⁻¹'o " => Order.Preimage

Preimage of an order relation under a function

Informal description

The notation `f ⁻¹'o s` represents the preimage of a relation `s` under a function `f`, which transfers the order relation `s` from the codomain to the domain. For any `x, y` in the domain, `x` is related to `y` under `f ⁻¹'o s` if and only if `f x` is related to `f y` under `s`.

Order.Preimage.decidable instance

(f : α → β) (s : β → β → Prop) [H : DecidableRel s] : DecidableRel (f ⁻¹'o s)

Full source

/-- The preimage of a decidable order is decidable. -/
instance Order.Preimage.decidable (f : α → β) (s : β → β → Prop) [H : DecidableRel s] :
    DecidableRel (f ⁻¹'o s) := fun _ _ ↦ H _ _

Decidability of Preimage Order Relations

Informal description

Given a function $f : \alpha \to \beta$ and a decidable relation $s$ on $\beta$, the preimage relation $f^{-1}o\, s$ on $\alpha$ (defined by $x \leq y \leftrightarrow f(x) \leq f(y)$) is also decidable.

le_trans' theorem

: b ≤ c → a ≤ b → a ≤ c

Full source

theorem le_trans' : b ≤ c → a ≤ b → a ≤ c :=
  flip le_trans

Transitivity of $\leq$ in a preorder

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b \leq c$ and $a \leq b$, then $a \leq c$.

lt_trans' theorem

: b < c → a < b → a < c

Full source

theorem lt_trans' : b < c → a < b → a < c :=
  flip lt_trans

Transitivity of Strict Inequality in Preorders

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b < c$ and $a < b$, then $a < c$.

lt_of_le_of_lt' theorem

: b ≤ c → a < b → a < c

Full source

theorem lt_of_le_of_lt' : b ≤ c → a < b → a < c :=
  flip lt_of_lt_of_le

Transitivity of Strict Inequality via Weak Inequality

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b \leq c$ and $a < b$, then $a < c$.

lt_of_lt_of_le' theorem

: b < c → a ≤ b → a < c

Full source

theorem lt_of_lt_of_le' : b < c → a ≤ b → a < c :=
  flip lt_of_le_of_lt

Transitivity of Strict and Non-Strict Inequalities: $b < c$ and $a \leq b$ implies $a < c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b < c$ and $a \leq b$, then $a < c$.

le_of_le_of_eq' theorem

: b ≤ c → a = b → a ≤ c

Full source

theorem le_of_le_of_eq' : b ≤ c → a = b → a ≤ c :=
  flip le_of_eq_of_le

Transitivity of $\leq$ with Equality

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b \leq c$ and $a = b$, then $a \leq c$.

le_of_eq_of_le' theorem

: b = c → a ≤ b → a ≤ c

Full source

theorem le_of_eq_of_le' : b = c → a ≤ b → a ≤ c :=
  flip le_of_le_of_eq

Transitivity of Inequality with Equality: $b = c \land a \leq b \implies a \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b = c$ and $a \leq b$, then $a \leq c$.

lt_of_lt_of_eq' theorem

: b < c → a = b → a < c

Full source

theorem lt_of_lt_of_eq' : b < c → a = b → a < c :=
  flip lt_of_eq_of_lt

Strict Inequality Preservation Under Equality: $b < c \land a = b \Rightarrow a < c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b < c$ and $a = b$, then $a < c$.

lt_of_eq_of_lt' theorem

: b = c → a < b → a < c

Full source

theorem lt_of_eq_of_lt' : b = c → a < b → a < c :=
  flip lt_of_lt_of_eq

Strict Inequality Preservation Under Equality Replacement

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b = c$ and $a < b$, then $a < c$.

not_lt_iff_not_le_or_ge theorem

: ¬a < b ↔ ¬a ≤ b ∨ b ≤ a

Full source

theorem not_lt_iff_not_le_or_ge : ¬a < b¬a < b ↔ ¬a ≤ b ∨ b ≤ a := by
  rw [lt_iff_le_not_le, Classical.not_and_iff_not_or_not, Classical.not_not]

Negation of Strict Inequality Equivalent to Negation of Non-Strict Inequality or Reverse Non-Strict Inequality

Informal description

For any elements $a$ and $b$ in a preorder, the statement $\neg (a < b)$ is equivalent to $\neg (a \leq b) \lor (b \leq a)$.

not_lt_iff_le_imp_le theorem

: ¬a < b ↔ (a ≤ b → b ≤ a)

Full source

lemma not_lt_iff_le_imp_le : ¬ a < b¬ a < b ↔ (a ≤ b → b ≤ a) := by
  simp [not_lt_iff_not_le_or_ge, or_iff_not_imp_left]

Negation of Strict Order Implies Antisymmetry Condition

Informal description

For any elements $a$ and $b$ in a preorder, the statement that $a$ is not less than $b$ is equivalent to the implication that if $a \leq b$ then $b \leq a$.

ge_of_eq theorem

(h : a = b) : b ≤ a

Full source

/-- If `x = y` then `y ≤ x`. Note: this lemma uses `y ≤ x` instead of `x ≥ y`, because `le` is used
almost exclusively in mathlib. -/
lemma ge_of_eq (h : a = b) : b ≤ a := le_of_eq h.symm

Reflexivity of $\leq$ via equality

Informal description

For any elements $a$ and $b$ in a preorder, if $a = b$ then $b \leq a$.

lt_self_iff_false theorem

(x : α) : x < x ↔ False

Full source

@[simp] lemma lt_self_iff_false (x : α) : x < x ↔ False := ⟨lt_irrefl x, False.elim⟩

Irreflexivity of Strict Order: $x < x \leftrightarrow \text{False}$

Informal description

For any element $x$ of a type $\alpha$ equipped with a strict order relation $<$, the statement $x < x$ is equivalent to false.

ne_of_not_le theorem

(h : ¬a ≤ b) : a ≠ b

Full source

theorem ne_of_not_le (h : ¬a ≤ b) : a ≠ b := fun hab ↦ h (le_of_eq hab)

Inequality from Non-Comparison: $\neg (a \leq b) \to a \neq b$

Informal description

If $a$ is not less than or equal to $b$ (i.e., $\neg (a \leq b)$), then $a$ is not equal to $b$ (i.e., $a \neq b$).

Eq.not_lt theorem

(hab : a = b) : ¬a < b

Full source

protected lemma Eq.not_lt (hab : a = b) : ¬a < b := fun h' ↦ h'.ne hab

Equality Implies Non-Strict-Inequality: $a = b \to \neg (a < b)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with a strict order relation $<$, if $a = b$, then $a$ is not less than $b$ (i.e., $\neg (a < b)$).

Eq.not_gt theorem

(hab : a = b) : ¬b < a

Full source

protected lemma Eq.not_gt (hab : a = b) : ¬b < a := hab.symm.not_lt

Equality Implies Non-Strict-Inequality (Dual): $a = b \to \neg (b < a)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with a strict order relation $<$, if $a = b$, then $b$ is not less than $a$ (i.e., $\neg (b < a)$).

le_of_subsingleton theorem

[Subsingleton α] : a ≤ b

Full source

@[simp] lemma le_of_subsingleton [Subsingleton α] : a ≤ b := (Subsingleton.elim a b).le

Subsingleton Implies All Elements Are Comparable

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements are equal), any two elements $a$ and $b$ satisfy $a \leq b$.

not_lt_of_subsingleton theorem

[Subsingleton α] : ¬a < b

Full source

lemma not_lt_of_subsingleton [Subsingleton α] : ¬a < b := (Subsingleton.elim a b).not_lt

No Strict Inequality in Subsingleton Types

Informal description

For any elements $a$ and $b$ in a type $\alpha$ that is a subsingleton (i.e., all elements of $\alpha$ are equal), the strict inequality $a < b$ does not hold.

LT.lt.false theorem

: a < a → False

Full source

protected theorem false : a < a → False := lt_irrefl a

Irreflexivity of Strict Order Relation

Informal description

For any element $a$ in a type with a strict order relation $<$, the statement $a < a$ is false.

LT.lt.ne' theorem

(h : a < b) : b ≠ a

Full source

theorem ne' (h : a < b) : b ≠ a := h.ne.symm

Inequality from Strict Order Relation

Informal description

For any elements $a$ and $b$ in a type with a strict order relation $<$, if $a < b$ then $b \neq a$.

le_of_forall_le theorem

(H : ∀ c, c ≤ a → c ≤ b) : a ≤ b

Full source

theorem le_of_forall_le (H : ∀ c, c ≤ a → c ≤ b) : a ≤ b := H _ le_rfl

Characterization of $\leq$ via Universal Property

Informal description

For any elements $a$ and $b$ in a preorder, if for every element $c$ the condition $c \leq a$ implies $c \leq b$, then $a \leq b$.

le_of_forall_ge theorem

(H : ∀ c, a ≤ c → b ≤ c) : b ≤ a

Full source

theorem le_of_forall_ge (H : ∀ c, a ≤ c → b ≤ c) : b ≤ a := H _ le_rfl

Implication of Universal Upper Bounds on Order Relation

Informal description

For any elements $a$ and $b$ in a partially ordered set, if for every element $c$ the condition $a \leq c$ implies $b \leq c$, then $b \leq a$.

forall_le_iff_le theorem

: (∀ ⦃c⦄, c ≤ a → c ≤ b) ↔ a ≤ b

Full source

theorem forall_le_iff_le : (∀ ⦃c⦄, c ≤ a → c ≤ b) ↔ a ≤ b :=
  ⟨le_of_forall_le, fun h _ hca ↦ le_trans hca h⟩

Universal Characterization of $\leq$ in Preorders

Informal description

For any elements $a$ and $b$ in a preorder, the following are equivalent: 1. For every element $c$, if $c \leq a$ then $c \leq b$. 2. $a \leq b$.

forall_le_iff_ge theorem

: (∀ ⦃c⦄, a ≤ c → b ≤ c) ↔ b ≤ a

Full source

theorem forall_le_iff_ge : (∀ ⦃c⦄, a ≤ c → b ≤ c) ↔ b ≤ a :=
  ⟨le_of_forall_ge, fun h _ hca ↦ le_trans h hca⟩

Universal Upper Bound Criterion for Order Relation

Informal description

For any elements $a$ and $b$ in a partially ordered set, the following are equivalent: 1. For every element $c$, if $a \leq c$ then $b \leq c$. 2. $b \leq a$.

le_implies_le_of_le_of_le theorem

(hca : c ≤ a) (hbd : b ≤ d) : a ≤ b → c ≤ d

Full source

/-- monotonicity of `≤` with respect to `→` -/
theorem le_implies_le_of_le_of_le (hca : c ≤ a) (hbd : b ≤ d) : a ≤ b → c ≤ d :=
  fun hab ↦ (hca.trans hab).trans hbd

Monotonicity of Partial Order with Respect to Implication

Informal description

For any elements $a, b, c, d$ in a partially ordered set, if $c \leq a$, $b \leq d$, and $a \leq b$, then $c \leq d$.

ge_antisymm theorem

: a ≤ b → b ≤ a → b = a

Full source

theorem ge_antisymm : a ≤ b → b ≤ a → b = a :=
  flip le_antisymm

Antisymmetry of Partial Order

Informal description

For any elements $a$ and $b$ in a partially ordered set, if $a \leq b$ and $b \leq a$, then $a = b$.

lt_of_le_of_ne' theorem

: a ≤ b → b ≠ a → a < b

Full source

theorem lt_of_le_of_ne' : a ≤ b → b ≠ a → a < b := fun h₁ h₂ ↦ lt_of_le_of_ne h₁ h₂.symm

Strict inequality from non-strict inequality and non-equality

Informal description

For any elements $a$ and $b$ in a partially ordered set, if $a \leq b$ and $b \neq a$, then $a < b$.

Ne.lt_of_le theorem

: a ≠ b → a ≤ b → a < b

Full source

theorem Ne.lt_of_le : a ≠ b → a ≤ b → a < b :=
  flip lt_of_le_of_ne

Strict Inequality from Non-Equal Elements in Partial Order

Informal description

For any two elements $a$ and $b$ in a partially ordered set, if $a \neq b$ and $a \leq b$, then $a < b$.

Ne.lt_of_le' theorem

: b ≠ a → a ≤ b → a < b

Full source

theorem Ne.lt_of_le' : b ≠ a → a ≤ b → a < b :=
  flip lt_of_le_of_ne'

Strict inequality from non-equality and non-strict inequality (variant)

Informal description

For any elements $a$ and $b$ in a partially ordered set, if $b \neq a$ and $a \leq b$, then $a < b$.

le_imp_eq_iff_le_imp_le theorem

: (a ≤ b → b = a) ↔ (a ≤ b → b ≤ a)

Full source

lemma le_imp_eq_iff_le_imp_le : (a ≤ b → b = a) ↔ (a ≤ b → b ≤ a) where
  mp h hab := (h hab).le
  mpr h hab := (h hab).antisymm hab

Equivalence of Antisymmetry Conditions in Partial Orders

Informal description

For any two elements $a$ and $b$ in a partially ordered set, the following are equivalent: 1. If $a \leq b$ then $b = a$. 2. If $a \leq b$ then $b \leq a$.

ge_imp_eq_iff_le_imp_le theorem

: (a ≤ b → a = b) ↔ (a ≤ b → b ≤ a)

Full source

lemma ge_imp_eq_iff_le_imp_le : (a ≤ b → a = b) ↔ (a ≤ b → b ≤ a) where
  mp h hab := (h hab).ge
  mpr h hab := hab.antisymm (h hab)

Equivalence of Equality and Symmetric Inequality Conditions in Partial Orders

Informal description

For any elements $a$ and $b$ in a partially ordered set, the following are equivalent: 1. If $a \leq b$ then $a = b$. 2. If $a \leq b$ then $b \leq a$.

LE.le.lt_iff_ne theorem

(h : a ≤ b) : a < b ↔ a ≠ b

Full source

theorem lt_iff_ne (h : a ≤ b) : a < b ↔ a ≠ b :=
  ⟨fun h ↦ h.ne, h.lt_of_ne⟩

Strict Inequality Under Non-Equality in Preorders

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the strict inequality $a < b$ holds if and only if $a \neq b$.

LE.le.gt_iff_ne theorem

(h : a ≤ b) : a < b ↔ b ≠ a

Full source

theorem gt_iff_ne (h : a ≤ b) : a < b ↔ b ≠ a :=
  ⟨fun h ↦ h.ne.symm, h.lt_of_ne'⟩

Strict Inequality Under Non-Equality (Symmetric Form) in Preorders

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the strict inequality $a < b$ holds if and only if $b \neq a$.

LE.le.not_lt_iff_eq theorem

(h : a ≤ b) : ¬a < b ↔ a = b

Full source

theorem not_lt_iff_eq (h : a ≤ b) : ¬a < b¬a < b ↔ a = b :=
  h.lt_iff_ne.not_left

Non-strict Inequality Implies Equality: $\neg(a < b) \leftrightarrow a = b$ under $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the statement $\neg(a < b)$ holds if and only if $a = b$.

LE.le.not_gt_iff_eq theorem

(h : a ≤ b) : ¬a < b ↔ b = a

Full source

theorem not_gt_iff_eq (h : a ≤ b) : ¬a < b¬a < b ↔ b = a :=
  h.gt_iff_ne.not_left

Non-strict Inequality Implies Equality: $\neg(a < b) \leftrightarrow b = a$ under $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the statement $\neg(a < b)$ holds if and only if $b = a$.

LE.le.le_iff_eq theorem

(h : a ≤ b) : b ≤ a ↔ b = a

Full source

theorem le_iff_eq (h : a ≤ b) : b ≤ a ↔ b = a :=
  ⟨fun h' ↦ h'.antisymm h, Eq.le⟩

Antisymmetry Condition for Partial Order: $b \leq a \leftrightarrow b = a$ under $a \leq b$

Informal description

For any two elements $a$ and $b$ in a partially ordered set, if $a \leq b$, then $b \leq a$ holds if and only if $b = a$.

LE.le.ge_iff_eq theorem

(h : a ≤ b) : b ≤ a ↔ a = b

Full source

theorem ge_iff_eq (h : a ≤ b) : b ≤ a ↔ a = b :=
  ⟨h.antisymm, Eq.ge⟩

Antisymmetry Condition for Partial Order: $b \leq a \leftrightarrow a = b$ under $a \leq b$

Informal description

For any two elements $a$ and $b$ in a partially ordered set, if $a \leq b$, then $b \leq a$ holds if and only if $a = b$.

Decidable.le_iff_eq_or_lt theorem

[DecidableLE α] : a ≤ b ↔ a = b ∨ a < b

Full source

protected theorem Decidable.le_iff_eq_or_lt [DecidableLE α] : a ≤ b ↔ a = b ∨ a < b :=
  Decidable.le_iff_lt_or_eq.trans or_comm

Decidable Less-Than-Or-Equal as Equality or Strict Less-Than

Informal description

For any two elements $a$ and $b$ in a type $\alpha$ with a decidable less-than-or-equal relation, $a \leq b$ holds if and only if either $a = b$ or $a < b$.

le_iff_eq_or_lt theorem

: a ≤ b ↔ a = b ∨ a < b

Full source

theorem le_iff_eq_or_lt : a ≤ b ↔ a = b ∨ a < b := le_iff_lt_or_eq.trans or_comm

Characterization of $\leq$ in terms of $=$ and $<$ in a preorder

Informal description

For any two elements $a$ and $b$ in a preorder, $a \leq b$ if and only if either $a = b$ or $a < b$.

lt_iff_le_and_ne theorem

: a < b ↔ a ≤ b ∧ a ≠ b

Full source

theorem lt_iff_le_and_ne : a < b ↔ a ≤ b ∧ a ≠ b :=
  ⟨fun h ↦ ⟨le_of_lt h, ne_of_lt h⟩, fun ⟨h1, h2⟩ ↦ h1.lt_of_ne h2⟩

Characterization of $<$ in terms of $\leq$ and $\neq$ in a preorder

Informal description

For any two elements $a$ and $b$ in a preorder, $a < b$ holds if and only if $a \leq b$ and $a \neq b$.

gt_or_eq_of_le theorem

(h : a ≤ b) : a < b ∨ b = a

Full source

theorem gt_or_eq_of_le (h : a ≤ b) : a < b ∨ b = a := (eq_or_gt_of_le h).symm

Trichotomy of Partial Order: $a \leq b$ implies $a < b$ or $b = a$

Informal description

For any two elements $a$ and $b$ in a partially ordered set, if $a \leq b$, then either $a < b$ or $b = a$.

Ne.le_iff_lt theorem

(h : a ≠ b) : a ≤ b ↔ a < b

Full source

theorem Ne.le_iff_lt (h : a ≠ b) : a ≤ b ↔ a < b := ⟨fun h' ↦ lt_of_le_of_ne h' h, fun h ↦ h.le⟩

Equivalence of Non-strict and Strict Order for Distinct Elements

Informal description

For any two distinct elements $a$ and $b$ in a linearly ordered type, the statement $a \leq b$ is equivalent to $a < b$. That is, $a \neq b$ implies $(a \leq b \leftrightarrow a < b)$.

Ne.not_le_or_not_le theorem

(h : a ≠ b) : ¬a ≤ b ∨ ¬b ≤ a

Full source

theorem Ne.not_le_or_not_le (h : a ≠ b) : ¬a ≤ b¬a ≤ b ∨ ¬b ≤ a := not_and_or.1 <| le_antisymm_iff.not.1 h

Non-comparable Elements in Linear Order

Informal description

For any two distinct elements $a$ and $b$ in a linearly ordered type, either $a$ is not less than or equal to $b$, or $b$ is not less than or equal to $a$. That is, $a \neq b$ implies $¬(a ≤ b) ∨ ¬(b ≤ a)$.

Decidable.ne_iff_lt_iff_le theorem

[DecidableEq α] : (a ≠ b ↔ a < b) ↔ a ≤ b

Full source

protected theorem Decidable.ne_iff_lt_iff_le [DecidableEq α] : (a ≠ b ↔ a < b) ↔ a ≤ b :=
  ⟨fun h ↦ Decidable.byCases le_of_eq (le_of_lt ∘ h.mp), fun h ↦ ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩

Equivalence of Inequality and Strict Order in Decidable Linear Orders

Informal description

For a type $\alpha$ with a decidable equality relation and a linear order, the following equivalence holds for any elements $a, b \in \alpha$: $$(a \neq b \leftrightarrow a < b) \leftrightarrow a \leq b.$$

ne_iff_lt_iff_le theorem

: (a ≠ b ↔ a < b) ↔ a ≤ b

Full source

@[simp]
theorem ne_iff_lt_iff_le : (a ≠ b ↔ a < b) ↔ a ≤ b :=
  haveI := Classical.dec
  Decidable.ne_iff_lt_iff_le

Equivalence of Inequality and Strict Order in Linear Orders: $(a \neq b \leftrightarrow a < b) \leftrightarrow a \leq b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type, the equivalence $(a \neq b \leftrightarrow a < b)$ holds if and only if $a \leq b$.

commutative_of_le theorem

{f : β → β → α} (comm : ∀ a b, f a b ≤ f b a) : ∀ a b, f a b = f b a

Full source

/-- To prove commutativity of a binary operation `○`, we only to check `a ○ b ≤ b ○ a` for all `a`,
`b`. -/
lemma commutative_of_le {f : β → β → α} (comm : ∀ a b, f a b ≤ f b a) : ∀ a b, f a b = f b a :=
  fun _ _ ↦ (comm _ _).antisymm <| comm _ _

Commutativity from Inequality Condition

Informal description

Let $f : \beta \to \beta \to \alpha$ be a binary operation. If for all $a, b \in \beta$ we have $f(a, b) \leq f(b, a)$, then $f$ is commutative, i.e., $f(a, b) = f(b, a)$ for all $a, b \in \beta$.

associative_of_commutative_of_le theorem

{f : α → α → α} (comm : Std.Commutative f) (assoc : ∀ a b c, f (f a b) c ≤ f a (f b c)) : Std.Associative f

Full source

/-- To prove associativity of a commutative binary operation `○`, we only to check
`(a ○ b) ○ c ≤ a ○ (b ○ c)` for all `a`, `b`, `c`. -/
lemma associative_of_commutative_of_le {f : α → α → α} (comm : Std.Commutative f)
    (assoc : ∀ a b c, f (f a b) c ≤ f a (f b c)) : Std.Associative f where
  assoc a b c :=
    le_antisymm (assoc _ _ _) <| by
      rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]
      exact assoc ..

Associativity from Commutativity and Inequality Condition

Informal description

Let $f : \alpha \to \alpha \to \alpha$ be a commutative binary operation. If for all $a, b, c \in \alpha$ we have $f(f(a, b), c) \leq f(a, f(b, c))$, then $f$ is associative.

LE.le.lt_or_le theorem

(h : a ≤ b) (c : α) : a < c ∨ c ≤ b

Full source

lemma lt_or_le (h : a ≤ b) (c : α) : a < c ∨ c ≤ b := (lt_or_ge a c).imp id h.trans'

Splitting Lemma for $\leq$ and $<$ in Partial Orders

Informal description

For any elements $a, b, c$ in a partially ordered set $\alpha$, if $a \leq b$, then either $a < c$ or $c \leq b$.

LE.le.le_or_lt theorem

(h : a ≤ b) (c : α) : a ≤ c ∨ c < b

Full source

lemma le_or_lt (h : a ≤ b) (c : α) : a ≤ c ∨ c < b := (le_or_gt a c).imp id h.trans_lt'

Splitting Lemma for $\leq$ and $<$ in Partial Orders

Informal description

For any elements $a, b, c$ in a partially ordered set $\alpha$, if $a \leq b$, then either $a \leq c$ or $c < b$.

LE.le.le_or_le theorem

(h : a ≤ b) (c : α) : a ≤ c ∨ c ≤ b

Full source

lemma le_or_le (h : a ≤ b) (c : α) : a ≤ c ∨ c ≤ b := (h.lt_or_le c).imp le_of_lt id

Splitting Property for $\leq$ in Partial Orders

Informal description

For any elements $a, b, c$ in a partially ordered set $\alpha$, if $a \leq b$, then either $a \leq c$ or $c \leq b$.

LT.lt.lt_or_lt theorem

(h : a < b) (c : α) : a < c ∨ c < b

Full source

lemma lt_or_lt (h : a < b) (c : α) : a < c ∨ c < b := (le_or_gt b c).imp h.trans_le id

Trichotomy-like Property for Strict Order

Informal description

For any elements $a$, $b$, and $c$ in a type $\alpha$ with a strict order relation $<$, if $a < b$, then either $a < c$ or $c < b$.

min_def' theorem

(a b : α) : min a b = if b ≤ a then b else a

Full source

theorem min_def' (a b : α) : min a b = if b ≤ a then b else a := by
  rw [min_def]
  rcases lt_trichotomy a b with (lt | eq | gt)
  · rw [if_pos lt.le, if_neg (not_le.mpr lt)]
  · rw [if_pos eq.le, if_pos eq.ge, eq]
  · rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]

Definition of Minimum via Conditional Expression

Informal description

For any two elements $a$ and $b$ in a type $\alpha$ with a partial order $\leq$, the minimum of $a$ and $b$ is equal to $b$ if $b \leq a$, and equal to $a$ otherwise. In other words, $\min(a, b) = \begin{cases} b & \text{if } b \leq a \\ a & \text{otherwise} \end{cases}$.

max_def' theorem

(a b : α) : max a b = if b ≤ a then a else b

Full source

theorem max_def' (a b : α) : max a b = if b ≤ a then a else b := by
  rw [max_def]
  rcases lt_trichotomy a b with (lt | eq | gt)
  · rw [if_pos lt.le, if_neg (not_le.mpr lt)]
  · rw [if_pos eq.le, if_pos eq.ge, eq]
  · rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]

Definition of Maximum via Conditional Expression

Informal description

For any two elements $a$ and $b$ in a type $\alpha$ with a partial order $\leq$, the maximum of $a$ and $b$ is equal to $a$ if $b \leq a$, and equal to $b$ otherwise. In other words, $\max(a, b) = \begin{cases} a & \text{if } b \leq a \\ b & \text{otherwise} \end{cases}$.

lt_of_not_le theorem

(h : ¬b ≤ a) : a < b

Full source

theorem lt_of_not_le (h : ¬b ≤ a) : a < b :=
  ((le_total _ _).resolve_right h).lt_of_not_le h

Strict inequality from negation of weak inequality

Informal description

For any two elements $a$ and $b$ in a partial order, if $b$ is not less than or equal to $a$, then $a$ is strictly less than $b$.

lt_iff_not_le theorem

: a < b ↔ ¬b ≤ a

Full source

theorem lt_iff_not_le : a < b ↔ ¬b ≤ a :=
  ⟨not_le_of_lt, lt_of_not_le⟩

Characterization of Strict Order via Negation of Weak Order

Informal description

For any two elements $a$ and $b$ in a partial order, $a < b$ if and only if $b$ is not less than or equal to $a$.

Ne.lt_or_lt theorem

(h : a ≠ b) : a < b ∨ b < a

Full source

theorem Ne.lt_or_lt (h : a ≠ b) : a < b ∨ b < a :=
  lt_or_gt_of_ne h

Non-Equal Elements in Linear Order are Comparable

Informal description

For any two elements $a$ and $b$ in a linear order, if $a \neq b$, then either $a < b$ or $b < a$.

lt_or_lt_iff_ne theorem

: a < b ∨ b < a ↔ a ≠ b

Full source

/-- A version of `ne_iff_lt_or_gt` with LHS and RHS reversed. -/
@[simp]
theorem lt_or_lt_iff_ne : a < b ∨ b < aa < b ∨ b < a ↔ a ≠ b :=
  ne_iff_lt_or_gt.symm

Inequality Equivalent to Strict Ordering in Linear Order

Informal description

For any two elements $a$ and $b$ in a linear order, $a < b$ or $b < a$ holds if and only if $a \neq b$.

not_lt_iff_eq_or_lt theorem

: ¬a < b ↔ a = b ∨ b < a

Full source

theorem not_lt_iff_eq_or_lt : ¬a < b¬a < b ↔ a = b ∨ b < a :=
  not_lt.trans <| Decidable.le_iff_eq_or_lt.trans <| or_congr eq_comm Iff.rfl

Negation of Strict Ordering Equivalent to Equality or Reverse Ordering

Informal description

For any two elements $a$ and $b$ in a linear order, the statement $\neg (a < b)$ is equivalent to $a = b$ or $b < a$.

exists_ge_of_linear theorem

(a b : α) : ∃ c, a ≤ c ∧ b ≤ c

Full source

theorem exists_ge_of_linear (a b : α) : ∃ c, a ≤ c ∧ b ≤ c :=
  match le_total a b with
  | Or.inl h => ⟨_, h, le_rfl⟩
  | Or.inr h => ⟨_, le_rfl, h⟩

Existence of Common Upper Bound in Linear Orders

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, there exists an element $c$ such that both $a \leq c$ and $b \leq c$ hold.

exists_forall_ge_and theorem

{p q : α → Prop} : (∃ i, ∀ j ≥ i, p j) → (∃ i, ∀ j ≥ i, q j) → ∃ i, ∀ j ≥ i, p j ∧ q j

Full source

lemma exists_forall_ge_and {p q : α → Prop} :
    (∃ i, ∀ j ≥ i, p j) → (∃ i, ∀ j ≥ i, q j) → ∃ i, ∀ j ≥ i, p j ∧ q j
  | ⟨a, ha⟩, ⟨b, hb⟩ =>
    let ⟨c, hac, hbc⟩ := exists_ge_of_linear a b
    ⟨c, fun _d hcd ↦ ⟨ha _ <| hac.trans hcd, hb _ <| hbc.trans hcd⟩⟩

Existence of Common Index for Eventually True Predicates in Linear Orders

Informal description

For any two predicates $p$ and $q$ on a linearly ordered type $\alpha$, if there exists an index $i_1$ such that $p(j)$ holds for all $j \geq i_1$, and an index $i_2$ such that $q(j)$ holds for all $j \geq i_2$, then there exists an index $i$ such that both $p(j)$ and $q(j)$ hold for all $j \geq i$.

le_of_forall_lt theorem

(H : ∀ c, c < a → c < b) : a ≤ b

Full source

theorem le_of_forall_lt (H : ∀ c, c < a → c < b) : a ≤ b :=
  le_of_not_lt fun h ↦ lt_irrefl _ (H _ h)

Inequality from Universal Comparison of Lesser Elements

Informal description

For any elements $a$ and $b$ in a linear order, if for every element $c$ such that $c < a$ implies $c < b$, then $a \leq b$.

forall_lt_iff_le theorem

: (∀ ⦃c⦄, c < a → c < b) ↔ a ≤ b

Full source

theorem forall_lt_iff_le : (∀ ⦃c⦄, c < a → c < b) ↔ a ≤ b :=
  ⟨le_of_forall_lt, fun h _ hca ↦ lt_of_lt_of_le hca h⟩

Universal Comparison of Lesser Elements Characterizes Inequality ($\forall c < a \Rightarrow c < b \leftrightarrow a \leq b$)

Informal description

For any elements $a$ and $b$ in a linear order, the following are equivalent: 1. For every element $c$, if $c < a$ then $c < b$. 2. $a \leq b$.

le_of_forall_lt' theorem

(H : ∀ c, a < c → b < c) : b ≤ a

Full source

theorem le_of_forall_lt' (H : ∀ c, a < c → b < c) : b ≤ a :=
  le_of_not_lt fun h ↦ lt_irrefl _ (H _ h)

Upper Bound Implication for Linear Order

Informal description

For any elements $a$ and $b$ in a linear order, if for every element $c$ the condition $a < c$ implies $b < c$, then $b \leq a$.

forall_lt_iff_le' theorem

: (∀ ⦃c⦄, a < c → b < c) ↔ b ≤ a

Full source

theorem forall_lt_iff_le' : (∀ ⦃c⦄, a < c → b < c) ↔ b ≤ a :=
  ⟨le_of_forall_lt', fun h _ hac ↦ lt_of_le_of_lt h hac⟩

Characterization of Upper Bound Condition in Linear Order: $(\forall c, a < c \to b < c) \leftrightarrow b \leq a$

Informal description

For any elements $a$ and $b$ in a linear order, the following are equivalent: 1. For every element $c$, if $a < c$ then $b < c$. 2. $b \leq a$.

ltByCases_lt theorem

(h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} : ltByCases x y h₁ h₂ h₃ = h₁ h

Full source

@[simp]
lemma ltByCases_lt (h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :
    ltByCases x y h₁ h₂ h₃ = h₁ h := dif_pos h

Evaluation of `ltByCases` in the Less-Than Case

Informal description

For any elements $x$ and $y$ in a linear order, if $x < y$, then the function `ltByCases` evaluates to the first provided case handler $h_1$ applied to the proof $h$ of $x < y$.

ltByCases_gt theorem

(h : y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} : ltByCases x y h₁ h₂ h₃ = h₃ h

Full source

@[simp]
lemma ltByCases_gt (h : y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :
    ltByCases x y h₁ h₂ h₃ = h₃ h := (dif_neg h.not_lt).trans (dif_pos h)

Evaluation of `ltByCases` in the Greater-Than Case

Informal description

For any elements $x$ and $y$ in a linear order, if $y < x$, then the function `ltByCases` evaluates to the third provided case handler $h_3$ applied to the proof $h$ of $y < x$.

ltByCases_eq theorem

(h : x = y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} : ltByCases x y h₁ h₂ h₃ = h₂ h

Full source

@[simp]
lemma ltByCases_eq (h : x = y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :
    ltByCases x y h₁ h₂ h₃ = h₂ h := (dif_neg h.not_lt).trans (dif_neg h.not_gt)

Evaluation of `ltByCases` in the Equality Case

Informal description

For any elements $x$ and $y$ in a linear order, if $x = y$, then the function `ltByCases` evaluates to the second provided case handler $h_2$ applied to the proof $h$ of $x = y$.

ltByCases_rec theorem

 {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : P) (hlt : (h : x < y) → h₁ h = p)
  (heq : (h : x = y) → h₂ h = p) (hgt : (h : y < x) → h₃ h = p) : ltByCases x y h₁ h₂ h₃ = p

Full source

lemma ltByCases_rec {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : P)
    (hlt : (h : x < y) → h₁ h = p) (heq : (h : x = y) → h₂ h = p)
    (hgt : (h : y < x) → h₃ h = p) :
    ltByCases x y h₁ h₂ h₃ = p :=
  ltByCases x y
    (fun h => ltByCases_lt h ▸ hlt h)
    (fun h => ltByCases_eq h ▸ heq h)
    (fun h => ltByCases_gt h ▸ hgt h)

Recursion Principle for `ltByCases` with Uniform Output

Informal description

For any elements $x$ and $y$ in a linear order, and for any case handlers $h_1$, $h_2$, $h_3$ corresponding to the cases $x < y$, $x = y$, and $y < x$ respectively, if there exists a value $p$ such that: 1. For every proof $h$ of $x < y$, $h_1(h) = p$, 2. For every proof $h$ of $x = y$, $h_2(h) = p$, 3. For every proof $h$ of $y < x$, $h_3(h) = p$, then the function `ltByCases x y h₁ h₂ h₃` evaluates to $p$.

ltByCases_eq_iff theorem

 {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {p : P} :
  ltByCases x y h₁ h₂ h₃ = p ↔ (∃ h, h₁ h = p) ∨ (∃ h, h₂ h = p) ∨ (∃ h, h₃ h = p)

Full source

lemma ltByCases_eq_iff {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {p : P} :
    ltByCasesltByCases x y h₁ h₂ h₃ = p ↔ (∃ h, h₁ h = p) ∨ (∃ h, h₂ h = p) ∨ (∃ h, h₃ h = p) := by
  refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)
  · simp only [ltByCases_lt, exists_prop_of_true, h, h.not_lt, not_false_eq_true,
    exists_prop_of_false, or_false, h.ne]
  · simp only [h, lt_self_iff_false, ltByCases_eq, not_false_eq_true,
    exists_prop_of_false, exists_prop_of_true, or_false, false_or]
  · simp only [ltByCases_gt, exists_prop_of_true, h, h.not_lt, not_false_eq_true,
    exists_prop_of_false, false_or, h.ne']

Characterization of `ltByCases` Output via Case Handlers

Informal description

For any elements $x$ and $y$ in a linear order, and for any case handlers $h_1$, $h_2$, $h_3$ corresponding to the cases $x < y$, $x = y$, and $y < x$ respectively, the value of `ltByCases x y h₁ h₂ h₃` equals $p$ if and only if there exists a proof $h$ in one of the three cases such that the corresponding handler applied to $h$ yields $p$.

ltByCases_congr theorem

 {x' y' : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {h₁' : x' < y' → P} {h₂' : x' = y' → P}
  {h₃' : y' < x' → P} (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x'))
  (hh'₁ : ∀ (h : x' < y'), h₁ (ltc.mpr h) = h₁' h)
  (hh'₂ : ∀ (h : x' = y'), h₂ ((eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc).mpr h) = h₂' h)
  (hh'₃ : ∀ (h : y' < x'), h₃ (gtc.mpr h) = h₃' h) : ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃'

Full source

lemma ltByCases_congr {x' y' : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
    {h₁' : x' < y' → P} {h₂' : x' = y' → P} {h₃' : y' < x' → P} (ltc : (x < y) ↔ (x' < y'))
    (gtc : (y < x) ↔ (y' < x')) (hh'₁ : ∀ (h : x' < y'), h₁ (ltc.mpr h) = h₁' h)
    (hh'₂ : ∀ (h : x' = y'), h₂ ((eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc).mpr h) = h₂' h)
    (hh'₃ : ∀ (h : y' < x'), h₃ (gtc.mpr h) = h₃' h) :
    ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃' := by
  refine ltByCases_rec _ (fun h => ?_) (fun h => ?_) (fun h => ?_)
  · rw [ltByCases_lt (ltc.mp h), hh'₁]
  · rw [eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc] at h
    rw [ltByCases_eq h, hh'₂]
  · rw [ltByCases_gt (gtc.mp h), hh'₃]

Congruence Property of Case Analysis on Linear Order: $\text{ltByCases } x y h_1 h_2 h_3 = \text{ltByCases } x' y' h'_1 h'_2 h'_3$ under Order-Preserving Conditions

Informal description

Let $\alpha$ be a type with a linear order, and let $x, y, x', y'$ be elements of $\alpha$. Suppose we have case handlers $h_1, h_2, h_3$ for the cases $x < y$, $x = y$, and $y < x$ respectively, and similarly $h'_1, h'_2, h'_3$ for $x' < y'$, $x' = y'$, and $y' < x'$. If: 1. The ordering relations satisfy $(x < y) \leftrightarrow (x' < y')$ and $(y < x) \leftrightarrow (y' < x')$, 2. For any proof $h$ of $x' < y'$, $h_1(\text{ltc.mpr } h) = h'_1(h)$, 3. For any proof $h$ of $x' = y'$, $h_2(\text{(eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc).mpr } h) = h'_2(h)$, 4. For any proof $h$ of $y' < x'$, $h_3(\text{gtc.mpr } h) = h'_3(h)$, then the case analysis functions satisfy $\text{ltByCases } x y h_1 h_2 h_3 = \text{ltByCases } x' y' h'_1 h'_2 h'_3$.

ltTrichotomy abbrev

(x y : α) (p q r : P)

Full source

/-- Perform a case-split on the ordering of `x` and `y` in a decidable linear order,
non-dependently. -/
abbrev ltTrichotomy (x y : α) (p q r : P) := ltByCases x y (fun _ => p) (fun _ => q) (fun _ => r)

Case-Split on Ordering Trichotomy in Linear Orders

Informal description

Given a decidable linear order on a type $\alpha$ and elements $x, y \in \alpha$, the abbreviation `ltTrichotomy` performs a case-split on the ordering of $x$ and $y$, returning one of three possible values $p$, $q$, or $r$ corresponding to the cases $x < y$, $x = y$, or $y < x$ respectively.

ltTrichotomy_lt theorem

(h : x < y) : ltTrichotomy x y p q r = p

Full source

@[simp]
lemma ltTrichotomy_lt (h : x < y) : ltTrichotomy x y p q r = p := ltByCases_lt h

Trichotomy Evaluation in Less-Than Case: $\text{ltTrichotomy}(x,y,p,q,r) = p$ when $x < y$

Informal description

For any elements $x$ and $y$ in a linear order, if $x < y$, then the trichotomy function `ltTrichotomy` evaluates to the first provided value $p$.

ltTrichotomy_gt theorem

(h : y < x) : ltTrichotomy x y p q r = r

Full source

@[simp]
lemma ltTrichotomy_gt (h : y < x) : ltTrichotomy x y p q r = r := ltByCases_gt h

Trichotomy Evaluation in Greater-Than Case: $\text{ltTrichotomy}(x,y,p,q,r) = r$ when $y < x$

Informal description

For any elements $x$ and $y$ in a linear order, if $y < x$, then the trichotomy function $\text{ltTrichotomy}(x, y, p, q, r)$ evaluates to the third provided value $r$.

ltTrichotomy_eq theorem

(h : x = y) : ltTrichotomy x y p q r = q

Full source

@[simp]
lemma ltTrichotomy_eq (h : x = y) : ltTrichotomy x y p q r = q := ltByCases_eq h

Trichotomy Evaluation in Equality Case: $\text{ltTrichotomy}(x,y,p,q,r) = q$ when $x = y$

Informal description

For any elements $x$ and $y$ in a linearly ordered type $\alpha$, if $x = y$, then the trichotomy function $\text{ltTrichotomy}(x, y, p, q, r)$ evaluates to the second provided value $q$.

ltTrichotomy_not_lt theorem

(h : ¬x < y) : ltTrichotomy x y p q r = if y < x then r else q

Full source

lemma ltTrichotomy_not_lt (h : ¬ x < y) :
    ltTrichotomy x y p q r = if y < x then r else q := ltByCases_not_lt h

Trichotomy Case-Split When Not Less Than

Informal description

For any elements $x$ and $y$ in a linearly ordered type $\alpha$, if $x$ is not less than $y$ (i.e., $\neg(x < y)$), then the trichotomy case-split `ltTrichotomy x y p q r` evaluates to $r$ if $y < x$, and to $q$ otherwise.

ltTrichotomy_not_gt theorem

(h : ¬y < x) : ltTrichotomy x y p q r = if x < y then p else q

Full source

lemma ltTrichotomy_not_gt (h : ¬ y < x) :
    ltTrichotomy x y p q r = if x < y then p else q := ltByCases_not_gt h

Trichotomy Case-Split When Greater-Than Fails: `ltTrichotomy x y p q r = if x < y then p else q` given $\neg(y < x)$

Informal description

For any elements $x$ and $y$ in a linearly ordered type $\alpha$, if $y$ is not less than $x$ (i.e., $\neg(y < x)$), then the trichotomy case-split evaluates to $p$ if $x < y$ and to $q$ otherwise. In other words, the expression `ltTrichotomy x y p q r` equals `if x < y then p else q` under the assumption $\neg(y < x)$.

ltTrichotomy_ne theorem

(h : x ≠ y) : ltTrichotomy x y p q r = if x < y then p else r

Full source

lemma ltTrichotomy_ne (h : x ≠ y) :
    ltTrichotomy x y p q r = if x < y then p else r := ltByCases_ne h

Trichotomy Case-Split for Distinct Elements: `ltTrichotomy x y p q r = if x < y then p else r` given $x \neq y$

Informal description

For any two distinct elements $x$ and $y$ in a linearly ordered type $\alpha$, the trichotomy case-split `ltTrichotomy x y p q r` evaluates to $p$ if $x < y$ and to $r$ otherwise. In other words, when $x \neq y$, the expression simplifies to `if x < y then p else r`.

ltTrichotomy_comm theorem

: ltTrichotomy x y p q r = ltTrichotomy y x r q p

Full source

lemma ltTrichotomy_comm : ltTrichotomy x y p q r = ltTrichotomy y x r q p := ltByCases_comm

Commutativity of Trichotomy Case-Split: `ltTrichotomy x y p q r = ltTrichotomy y x r q p`

Informal description

For any elements $x$ and $y$ in a linearly ordered type $\alpha$, the trichotomy case-split `ltTrichotomy x y p q r` is equal to `ltTrichotomy y x r q p`. In other words, swapping $x$ and $y$ in the trichotomy case-split swaps the results for the less-than and greater-than cases while keeping the equal case result unchanged.

ltTrichotomy_self theorem

{p : P} : ltTrichotomy x y p p p = p

Full source

lemma ltTrichotomy_self {p : P} : ltTrichotomy x y p p p = p :=
  ltByCases_rec p (fun _ => rfl) (fun _ => rfl) (fun _ => rfl)

Trichotomy Case-Split with Uniform Output: `ltTrichotomy x y p p p = p`

Informal description

For any elements $x$ and $y$ in a linearly ordered type $\alpha$ and any value $p$, the trichotomy case-split `ltTrichotomy x y p p p` evaluates to $p$ regardless of the ordering between $x$ and $y$.

ltTrichotomy_eq_iff theorem

: ltTrichotomy x y p q r = s ↔ (x < y ∧ p = s) ∨ (x = y ∧ q = s) ∨ (y < x ∧ r = s)

Full source

lemma ltTrichotomy_eq_iff : ltTrichotomyltTrichotomy x y p q r = s ↔
    (x < y ∧ p = s) ∨ (x = y ∧ q = s) ∨ (y < x ∧ r = s) := by
  refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)
  · simp only [ltTrichotomy_lt, false_and, true_and, or_false, h, h.not_lt, h.ne]
  · simp only [ltTrichotomy_eq, false_and, true_and, or_false, false_or, h, lt_irrefl]
  · simp only [ltTrichotomy_gt, false_and, true_and, false_or, h, h.not_lt, h.ne']

Characterization of Trichotomy Function Evaluation: $\text{ltTrichotomy}(x,y,p,q,r) = s$ iff $x < y$ and $p = s$, or $x = y$ and $q = s$, or $y < x$ and $r = s$

Informal description

For any elements $x$ and $y$ in a linearly ordered type $\alpha$, and for any values $p, q, r, s$, the trichotomy function $\text{ltTrichotomy}(x, y, p, q, r)$ evaluates to $s$ if and only if one of the following holds: 1. $x < y$ and $p = s$, or 2. $x = y$ and $q = s$, or 3. $y < x$ and $r = s$.

ltTrichotomy_congr theorem

 {x' y' : α} {p' q' r' : P} (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x')) (hh'₁ : x' < y' → p = p')
  (hh'₂ : x' = y' → q = q') (hh'₃ : y' < x' → r = r') : ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r'

Full source

lemma ltTrichotomy_congr {x' y' : α} {p' q' r' : P} (ltc : (x < y) ↔ (x' < y'))
    (gtc : (y < x) ↔ (y' < x')) (hh'₁ : x' < y' → p = p')
    (hh'₂ : x' = y' → q = q') (hh'₃ : y' < x' → r = r') :
    ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r' :=
  ltByCases_congr ltc gtc hh'₁ hh'₂ hh'₃

Congruence of Trichotomy Case-Split under Order-Preserving Conditions: $\text{ltTrichotomy}(x,y,p,q,r) = \text{ltTrichotomy}(x',y',p',q',r')$

Informal description

Let $\alpha$ be a type with a linear order, and let $x, y, x', y'$ be elements of $\alpha$. Suppose we have values $p, q, r, p', q', r'$ of type $P$. If: 1. The ordering relations satisfy $(x < y) \leftrightarrow (x' < y')$ and $(y < x) \leftrightarrow (y' < x')$, 2. For any proof that $x' < y'$, we have $p = p'$, 3. For any proof that $x' = y'$, we have $q = q'$, 4. For any proof that $y' < x'$, we have $r = r'$, then the trichotomy case-split functions satisfy $\text{ltTrichotomy}(x, y, p, q, r) = \text{ltTrichotomy}(x', y', p', q', r')$.

min_rec theorem

(ha : a ≤ b → p a) (hb : b ≤ a → p b) : p (min a b)

Full source

lemma min_rec (ha : a ≤ b → p a) (hb : b ≤ a → p b) : p (min a b) := by
  obtain hab | hba := le_total a b <;> simp [min_eq_left, min_eq_right, *]

Recursion Principle for Minimum Element

Informal description

For any two elements $a$ and $b$ in a partially ordered set, and for any predicate $p$, if $p(a)$ holds whenever $a \leq b$ and $p(b)$ holds whenever $b \leq a$, then $p(\min(a, b))$ holds.

max_rec theorem

(ha : b ≤ a → p a) (hb : a ≤ b → p b) : p (max a b)

Full source

lemma max_rec (ha : b ≤ a → p a) (hb : a ≤ b → p b) : p (max a b) := by
  obtain hab | hba := le_total a b <;> simp [max_eq_left, max_eq_right, *]

Recursion Principle for Maximum Element

Informal description

For any elements $a$ and $b$ in a partially ordered set, and for any predicate $p$, if $p(a)$ holds whenever $b \leq a$ and $p(b)$ holds whenever $a \leq b$, then $p(\max(a, b))$ holds.

min_rec' theorem

(p : α → Prop) (ha : p a) (hb : p b) : p (min a b)

Full source

lemma min_rec' (p : α → Prop) (ha : p a) (hb : p b) : p (min a b) :=
  min_rec (fun _ ↦ ha) fun _ ↦ hb

Minimum Element Preserves Predicate

Informal description

For any predicate $p$ on a type $\alpha$ with a partial order, and for any elements $a, b \in \alpha$, if $p(a)$ and $p(b)$ both hold, then $p(\min(a, b))$ also holds.

max_rec' theorem

(p : α → Prop) (ha : p a) (hb : p b) : p (max a b)

Full source

lemma max_rec' (p : α → Prop) (ha : p a) (hb : p b) : p (max a b) :=
  max_rec (fun _ ↦ ha) fun _ ↦ hb

Predicate Preservation under Maximum Operation

Informal description

For any predicate $p$ on a type $\alpha$ with a linear order, and for any elements $a, b \in \alpha$, if $p(a)$ and $p(b)$ both hold, then $p(\max(a, b))$ holds.

min_def_lt theorem

(a b : α) : min a b = if a < b then a else b

Full source

lemma min_def_lt (a b : α) : min a b = if a < b then a else b := by
  rw [min_comm, min_def, ← ite_not]; simp only [not_le]

Definition of Minimum via Strict Order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the minimum of $a$ and $b$ is equal to $a$ if $a < b$, and $b$ otherwise. In other words, $\min(a, b) = \begin{cases} a & \text{if } a < b \\ b & \text{otherwise} \end{cases}$.

max_def_lt theorem

(a b : α) : max a b = if a < b then b else a

Full source

lemma max_def_lt (a b : α) : max a b = if a < b then b else a := by
  rw [max_comm, max_def, ← ite_not]; simp only [not_le]

Definition of Maximum via Strict Order: $\max(a, b) = \text{if } a < b \text{ then } b \text{ else } a$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the maximum of $a$ and $b$ is equal to $b$ if $a < b$, and $a$ otherwise. In other words, $\max(a, b) = \begin{cases} b & \text{if } a < b \\ a & \text{otherwise} \end{cases}$.

lt_imp_lt_of_le_imp_le theorem

{β} [LinearOrder α] [Preorder β] {a b : α} {c d : β} (H : a ≤ b → c ≤ d) (h : d < c) : b < a

Full source

lemma lt_imp_lt_of_le_imp_le {β} [LinearOrder α] [Preorder β] {a b : α} {c d : β}
    (H : a ≤ b → c ≤ d) (h : d < c) : b < a :=
  lt_of_not_le fun h' ↦ (H h').not_lt h

Strict Inequality Reversal under Order-Preserving Implication

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ a preordered type. For any elements $a, b \in \alpha$ and $c, d \in \beta$, if the implication $a \leq b \rightarrow c \leq d$ holds and $d < c$, then $b < a$.

le_imp_le_iff_lt_imp_lt theorem

{β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} : a ≤ b → c ≤ d ↔ d < c → b < a

Full source

lemma le_imp_le_iff_lt_imp_lt {β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} :
    a ≤ b → c ≤ d ↔ d < c → b < a :=
  ⟨lt_imp_lt_of_le_imp_le, le_imp_le_of_lt_imp_lt⟩

Equivalence of Order-Preserving and Strict Order-Reversing Implications in Linear Orders

Informal description

Let $\alpha$ and $\beta$ be linearly ordered types. For any elements $a, b \in \alpha$ and $c, d \in \beta$, the implication $a \leq b \rightarrow c \leq d$ holds if and only if the implication $d < c \rightarrow b < a$ holds.

lt_iff_lt_of_le_iff_le' theorem

 {β} [Preorder α] [Preorder β] {a b : α} {c d : β} (H : a ≤ b ↔ c ≤ d) (H' : b ≤ a ↔ d ≤ c) : b < a ↔ d < c

Full source

lemma lt_iff_lt_of_le_iff_le' {β} [Preorder α] [Preorder β] {a b : α} {c d : β}
    (H : a ≤ b ↔ c ≤ d) (H' : b ≤ a ↔ d ≤ c) : b < a ↔ d < c :=
  lt_iff_le_not_le.trans <| (and_congr H' (not_congr H)).trans lt_iff_le_not_le.symm

Strict Inequality Equivalence under Order Isomorphism

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $a, b \in \alpha$ and $c, d \in \beta$. Given that $a \leq b$ if and only if $c \leq d$, and $b \leq a$ if and only if $d \leq c$, then $b < a$ if and only if $d < c$.

lt_iff_lt_of_le_iff_le theorem

{β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} (H : a ≤ b ↔ c ≤ d) : b < a ↔ d < c

Full source

lemma lt_iff_lt_of_le_iff_le {β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β}
    (H : a ≤ b ↔ c ≤ d) : b < a ↔ d < c := not_le.symm.trans <| (not_congr H).trans <| not_le

Strict Inequality Equivalence under Order-Preserving Condition

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets, and let $a, b \in \alpha$ and $c, d \in \beta$. Given that $a \leq b$ if and only if $c \leq d$, then $b < a$ if and only if $d < c$.

le_iff_le_iff_lt_iff_lt theorem

{β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} : (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)

Full source

lemma le_iff_le_iff_lt_iff_lt {β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} :
    (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
  ⟨lt_iff_lt_of_le_iff_le, fun H ↦ not_lt.symm.trans <| (not_congr H).trans <| not_lt⟩

Equivalence of Order Relations and Their Strict Counterparts in Linear Orders

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets, and let $a, b \in \alpha$ and $c, d \in \beta$. Then the following are equivalent: 1. The inequality $a \leq b$ holds if and only if $c \leq d$ holds. 2. The strict inequality $b < a$ holds if and only if $d < c$ holds.

rel_imp_eq_of_rel_imp_le theorem

 [PartialOrder β] (r : α → α → Prop) [IsSymm α r] {f : α → β} (h : ∀ a b, r a b → f a ≤ f b) {a b : α} :
  r a b → f a = f b

Full source

/-- A symmetric relation implies two values are equal, when it implies they're less-equal. -/
lemma rel_imp_eq_of_rel_imp_le [PartialOrder β] (r : α → α → Prop) [IsSymm α r] {f : α → β}
    (h : ∀ a b, r a b → f a ≤ f b) {a b : α} : r a b → f a = f b := fun hab ↦
  le_antisymm (h a b hab) (h b a <| symm hab)

Symmetric Relation Implies Equality under Monotonicity Condition

Informal description

Let $r$ be a symmetric relation on a type $\alpha$, and let $\beta$ be a partially ordered set. Given a function $f : \alpha \to \beta$ such that for any $a, b \in \alpha$, $r(a, b)$ implies $f(a) \leq f(b)$, then for any $a, b \in \alpha$ related by $r$, we have $f(a) = f(b)$.

Preorder.toLE_injective theorem

: Function.Injective (@Preorder.toLE α)

Full source

@[ext]
lemma Preorder.toLE_injective : Function.Injective (@Preorder.toLE α) :=
  fun
  | { lt := A_lt, lt_iff_le_not_le := A_iff, .. },
    { lt := B_lt, lt_iff_le_not_le := B_iff, .. } => by
    rintro ⟨⟩
    have : A_lt = B_lt := by
      funext a b
      rw [A_iff, B_iff]
    cases this
    congr

Injectivity of Preorder-to-LE Mapping

Informal description

The function that maps a preorder structure on a type $\alpha$ to its corresponding "less than or equal to" relation is injective. In other words, if two preorders on $\alpha$ induce the same $\leq$ relation, then the preorders must be equal.

PartialOrder.toPreorder_injective theorem

: Function.Injective (@PartialOrder.toPreorder α)

Full source

@[ext]
lemma PartialOrder.toPreorder_injective : Function.Injective (@PartialOrder.toPreorder α) := by
  rintro ⟨⟩ ⟨⟩ ⟨⟩; congr

Injectivity of Preorder Structure from Partial Order

Informal description

The function that maps a partial order structure on a type $\alpha$ to its underlying preorder structure is injective. In other words, if two partial orders on $\alpha$ induce the same preorder, then they must be equal.

LinearOrder.toPartialOrder_injective theorem

: Function.Injective (@LinearOrder.toPartialOrder α)

Full source

@[ext]
lemma LinearOrder.toPartialOrder_injective : Function.Injective (@LinearOrder.toPartialOrder α) :=
  fun
  | { le := A_le, lt := A_lt,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT
      min := A_min, max := A_max, min_def := A_min_def, max_def := A_max_def,
      compare := A_compare, compare_eq_compareOfLessAndEq := A_compare_canonical, .. },
    { le := B_le, lt := B_lt,
      toDecidableLE := B_decidableLE, toDecidableEq := B_decidableEq, toDecidableLT := B_decidableLT
      min := B_min, max := B_max, min_def := B_min_def, max_def := B_max_def,
      compare := B_compare, compare_eq_compareOfLessAndEq := B_compare_canonical, .. } => by
    rintro ⟨⟩
    obtain rfl : A_decidableLE = B_decidableLE := Subsingleton.elim _ _
    obtain rfl : A_decidableEq = B_decidableEq := Subsingleton.elim _ _
    obtain rfl : A_decidableLT = B_decidableLT := Subsingleton.elim _ _
    have : A_min = B_min := by
      funext a b
      exact (A_min_def _ _).trans (B_min_def _ _).symm
    cases this
    have : A_max = B_max := by
      funext a b
      exact (A_max_def _ _).trans (B_max_def _ _).symm
    cases this
    have : A_compare = B_compare := by
      funext a b
      exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
    congr

Injectivity of Partial Order Structure from Linear Order

Informal description

The function that maps a linear order structure on a type $\alpha$ to its underlying partial order structure is injective. In other words, if two linear orders on $\alpha$ induce the same partial order, then they must be equal.

Preorder.ext theorem

 {A B : Preorder α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y) :
  A = B

Full source

lemma Preorder.ext {A B : Preorder α} (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) : A = B := by
  ext x y; exact H x y

Extensionality of Preorder Structures

Informal description

Let $A$ and $B$ be two preorder structures on a type $\alpha$. If for all $x, y \in \alpha$, the relation $x \leq y$ holds in $A$ if and only if it holds in $B$, then $A$ and $B$ are equal.

PartialOrder.ext theorem

 {A B : PartialOrder α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y) :
  A = B

Full source

lemma PartialOrder.ext {A B : PartialOrder α} (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) :
    A = B := by ext x y; exact H x y

Extensionality of Partial Order Structures

Informal description

Let $A$ and $B$ be two partial order structures on a type $\alpha$. If for all $x, y \in \alpha$, the relation $x \leq y$ holds in $A$ if and only if it holds in $B$, then $A$ and $B$ are equal.

PartialOrder.ext_lt theorem

 {A B : PartialOrder α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x < y) ↔
        x < y) :
  A = B

Full source

lemma PartialOrder.ext_lt {A B : PartialOrder α} (H : ∀ x y : α, (haveI := A; x < y) ↔ x < y) :
    A = B := by ext x y; rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]

Extensionality of Partial Orders via Strict Inequality

Informal description

Let $A$ and $B$ be two partial order structures on a type $\alpha$. If for all $x, y \in \alpha$, the relation $x < y$ holds in $A$ if and only if it holds in $B$, then $A$ and $B$ are equal.

LinearOrder.ext theorem

 {A B : LinearOrder α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y) :
  A = B

Full source

lemma LinearOrder.ext {A B : LinearOrder α} (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) :
    A = B := by ext x y; exact H x y

Extensionality of Linear Order Structures

Informal description

Let $A$ and $B$ be two linear order structures on a type $\alpha$. If for all $x, y \in \alpha$, the relation $x \leq y$ holds in $A$ if and only if it holds in $B$, then $A$ and $B$ are equal.

LinearOrder.ext_lt theorem

 {A B : LinearOrder α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x < y) ↔
        x < y) :
  A = B

Full source

lemma LinearOrder.ext_lt {A B : LinearOrder α} (H : ∀ x y : α, (haveI := A; x < y) ↔ x < y) :
    A = B := LinearOrder.toPartialOrder_injective (PartialOrder.ext_lt H)

Extensionality of Linear Orders via Strict Inequality

Informal description

Let $A$ and $B$ be two linear order structures on a type $\alpha$. If for all $x, y \in \alpha$, the relation $x < y$ holds in $A$ if and only if it holds in $B$, then $A$ and $B$ are equal.

OrderDual definition

(α : Type*) : Type _

Full source

/-- Type synonym to equip a type with the dual order: `≤` means `≥` and `<` means `>`. `αᵒᵈ` is
notation for `OrderDual α`. -/
def OrderDual (α : Type*) : Type _ :=
  α

Order Dual

Informal description

The type synonym `OrderDual α` equips a type `α` with the dual order, where `≤` is interpreted as `≥` and `<` is interpreted as `>`. The notation `αᵒᵈ` is used to denote `OrderDual α`.

term_ᵒᵈ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:max α "ᵒᵈ" => OrderDual α

Order dual notation

Informal description

The notation `αᵒᵈ` represents the order dual of type `α`, which is a type synonym that reverses all inequality relations (≤ and <) of the original type.

OrderDual.instNonempty instance

(α : Type*) [h : Nonempty α] : Nonempty αᵒᵈ

Full source

instance (α : Type*) [h : Nonempty α] : Nonempty αᵒᵈ :=
  h

Nonempty Order Dual

Informal description

For any type $\alpha$ that is nonempty, its order dual $\alpha^\text{ᵒᵈ}$ is also nonempty.

OrderDual.instSubsingleton instance

(α : Type*) [h : Subsingleton α] : Subsingleton αᵒᵈ

Full source

instance (α : Type*) [h : Subsingleton α] : Subsingleton αᵒᵈ :=
  h

Subsingleton Property of Order Duals

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements are equal), its order dual $\alpha^\text{ᵒᵈ}$ is also a subsingleton.

OrderDual.instLE instance

(α : Type*) [LE α] : LE αᵒᵈ

Full source

instance (α : Type*) [LE α] : LE αᵒᵈ :=
  ⟨fun x y : α ↦ y ≤ x⟩

Preorder Structure on Order Dual

Informal description

For any type $\alpha$ equipped with a preorder (reflexive and transitive relation $\leq$), the order dual $\alpha^{\text{op}}$ is also equipped with a preorder where $x \leq y$ in $\alpha^{\text{op}}$ means $y \leq x$ in $\alpha$.

OrderDual.instLT instance

(α : Type*) [LT α] : LT αᵒᵈ

Full source

instance (α : Type*) [LT α] : LT αᵒᵈ :=
  ⟨fun x y : α ↦ y < x⟩

Strict Order on the Order Dual

Informal description

For any type $\alpha$ equipped with a strict order relation $<$, the order dual $\alpha^{\text{op}}$ is also equipped with a strict order relation, where $a <^{\text{op}} b$ is defined as $b < a$.

OrderDual.instOrd instance

(α : Type*) [Ord α] : Ord αᵒᵈ

Full source

instance instOrd (α : Type*) [Ord α] : Ord αᵒᵈ where
  compare := fun (a b : α) ↦ compare b a

Order Dual Inherits Order Structure

Informal description

For any type $\alpha$ equipped with an order relation (via the `Ord` typeclass), the order dual $\alpha^\text{op}$ also carries a canonical order relation where all inequalities are reversed.

OrderDual.instSup instance

(α : Type*) [Min α] : Max αᵒᵈ

Full source

instance instSup (α : Type*) [Min α] : Max αᵒᵈ :=
  ⟨((· ⊓ ·) : α → α → α)⟩

Maximum Operation on Order Dual via Minimum

Informal description

For any type $\alpha$ with a minimum operation, the order dual $\alpha^{\text{op}}$ has a maximum operation where the maximum in $\alpha^{\text{op}}$ corresponds to the minimum in $\alpha$.

OrderDual.instInf instance

(α : Type*) [Max α] : Min αᵒᵈ

Full source

instance instInf (α : Type*) [Max α] : Min αᵒᵈ :=
  ⟨((· ⊔ ·) : α → α → α)⟩

Minimum Operation on Order Dual via Maximum

Informal description

For any type $\alpha$ equipped with a maximum operation $\max$, the order dual $\alpha^{\text{op}}$ has a minimum operation $\min$ where $\min x y$ in $\alpha^{\text{op}}$ corresponds to $\max x y$ in $\alpha$.

OrderDual.instPreorder instance

(α : Type*) [Preorder α] : Preorder αᵒᵈ

Full source

instance instPreorder (α : Type*) [Preorder α] : Preorder αᵒᵈ where
  le_refl := fun _ ↦ le_refl _
  le_trans := fun _ _ _ hab hbc ↦ hbc.trans hab
  lt_iff_le_not_le := fun _ _ ↦ lt_iff_le_not_le

Preorder Structure on Order Dual

Informal description

For any type $\alpha$ equipped with a preorder (a reflexive and transitive relation $\leq$), the order dual $\alpha^{\text{op}}$ is also equipped with a preorder where $x \leq y$ in $\alpha^{\text{op}}$ means $y \leq x$ in $\alpha$.

OrderDual.instPartialOrder instance

(α : Type*) [PartialOrder α] : PartialOrder αᵒᵈ

Full source

instance instPartialOrder (α : Type*) [PartialOrder α] : PartialOrder αᵒᵈ where
  __ := inferInstanceAs (Preorder αᵒᵈ)
  le_antisymm := fun a b hab hba ↦ @le_antisymm α _ a b hba hab

Partial Order Structure on Order Dual

Informal description

For any type $\alpha$ equipped with a partial order (a reflexive, transitive, and antisymmetric relation $\leq$), the order dual $\alpha^{\text{op}}$ is also equipped with a partial order where $x \leq y$ in $\alpha^{\text{op}}$ means $y \leq x$ in $\alpha$.

OrderDual.instLinearOrder instance

(α : Type*) [LinearOrder α] : LinearOrder αᵒᵈ

Full source

instance instLinearOrder (α : Type*) [LinearOrder α] : LinearOrder αᵒᵈ where
  __ := inferInstanceAs (PartialOrder αᵒᵈ)
  __ := inferInstanceAs (Ord αᵒᵈ)
  le_total := fun a b : α ↦ le_total b a
  max := fun a b ↦ (min a b : α)
  min := fun a b ↦ (max a b : α)
  min_def := fun a b ↦ show (max .. : α) = _ by rw [max_comm, max_def]; rfl
  max_def := fun a b ↦ show (min .. : α) = _ by rw [min_comm, min_def]; rfl
  toDecidableLE := (inferInstance : DecidableRel (fun a b : α ↦ b ≤ a))
  toDecidableLT := (inferInstance : DecidableRel (fun a b : α ↦ b < a))
  toDecidableEq := (inferInstance : DecidableEq α)
  compare_eq_compareOfLessAndEq a b := by
    simp only [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]
    rfl

Linear Order Structure on Order Dual

Informal description

For any type $\alpha$ equipped with a linear order (a total, reflexive, transitive, and antisymmetric relation $\leq$), the order dual $\alpha^{\text{op}}$ is also equipped with a linear order where $x \leq y$ in $\alpha^{\text{op}}$ means $y \leq x$ in $\alpha$.

LinearOrder.swap definition

(α : Type*) (_ : LinearOrder α) : LinearOrder α

Full source

/-- The opposite linear order to a given linear order -/
def _root_.LinearOrder.swap (α : Type*) (_ : LinearOrder α) : LinearOrder α :=
  inferInstanceAs <| LinearOrder (OrderDual α)

Swapped linear order

Informal description

Given a type $\alpha$ with a linear order, the function constructs a linear order on $\alpha$ by swapping the order relation, i.e., $x \leq y$ in the swapped order if and only if $y \leq x$ in the original order. This is equivalent to the linear order structure on the order dual $\alpha^{\text{op}}$.

OrderDual.instInhabited instance

: ∀ [Inhabited α], Inhabited αᵒᵈ

Full source

instance : ∀ [Inhabited α], Inhabited αᵒᵈ := fun [x : Inhabited α] => x

Inhabitedness of Order Duals

Informal description

For any type $\alpha$ with an inhabited instance, the order dual $\alpha^{\text{op}}$ is also inhabited.

OrderDual.Ord.dual_dual theorem

(α : Type*) [H : Ord α] : OrderDual.instOrd αᵒᵈ = H

Full source

theorem Ord.dual_dual (α : Type*) [H : Ord α] : OrderDual.instOrd αᵒᵈ = H :=
  rfl

Double Dual Order Structure Equals Original

Informal description

For any type $\alpha$ equipped with an order structure `H : Ord α`, the order structure on the double dual $\alpha^{\text{op}\text{op}}$ (i.e., the order dual of the order dual of $\alpha$) is equal to the original order structure `H$.

OrderDual.Preorder.dual_dual theorem

(α : Type*) [H : Preorder α] : OrderDual.instPreorder αᵒᵈ = H

Full source

theorem Preorder.dual_dual (α : Type*) [H : Preorder α] : OrderDual.instPreorder αᵒᵈ = H :=
  rfl

Double Dual Preorder Structure Equals Original

Informal description

For any type $\alpha$ equipped with a preorder structure $H$, the preorder structure on the order dual $\alpha^{\text{op}}$ is equal to $H$ when dualized again. In other words, the double dual preorder structure coincides with the original preorder structure.

OrderDual.instPartialOrder.dual_dual theorem

(α : Type*) [H : PartialOrder α] : OrderDual.instPartialOrder αᵒᵈ = H

Full source

theorem instPartialOrder.dual_dual (α : Type*) [H : PartialOrder α] :
    OrderDual.instPartialOrder αᵒᵈ = H :=
  rfl

Double Dual Partial Order Structure Equals Original

Informal description

For any type $\alpha$ equipped with a partial order $H$, the partial order structure on the order dual $\alpha^{\text{op}}$ is equal to $H$ when dualized again. In other words, the double dual partial order structure coincides with the original partial order structure.

OrderDual.instLinearOrder.dual_dual theorem

(α : Type*) [H : LinearOrder α] : OrderDual.instLinearOrder αᵒᵈ = H

Full source

theorem instLinearOrder.dual_dual (α : Type*) [H : LinearOrder α] :
    OrderDual.instLinearOrder αᵒᵈ = H :=
  rfl

Double Dual Linear Order Structure Equals Original

Informal description

For any type $\alpha$ equipped with a linear order $H$, the linear order structure on the order dual $\alpha^{\text{op}}$ is equal to $H$ when dualized again. In other words, the double dual linear order structure coincides with the original linear order structure.

Prop.hasCompl instance

: HasCompl Prop

Full source

instance Prop.hasCompl : HasCompl Prop :=
  ⟨Not⟩

Complement Operation on Propositions

Informal description

The type of propositions `Prop` has a complement operation, where for any proposition `P`, its complement `Pᶜ` is the negation of `P`.

Pi.hasCompl instance

[∀ i, HasCompl (π i)] : HasCompl (∀ i, π i)

Full source

instance Pi.hasCompl [∀ i, HasCompl (π i)] : HasCompl (∀ i, π i) :=
  ⟨fun x i ↦ (x i)ᶜ⟩

Pointwise Complement Operation on Product Types

Informal description

For any family of types $\pi_i$ each equipped with a complement operation, the product type $\forall i, \pi_i$ inherits a complement operation defined pointwise.

Pi.compl_def theorem

[∀ i, HasCompl (π i)] (x : ∀ i, π i) : xᶜ = fun i ↦ (x i)ᶜ

Full source

theorem Pi.compl_def [∀ i, HasCompl (π i)] (x : ∀ i, π i) :
    xᶜ = fun i ↦ (x i)ᶜ :=
  rfl

Pointwise Complement of a Function

Informal description

For any family of types $\pi_i$ each equipped with a complement operation, the complement of a function $x : \forall i, \pi_i$ is the function defined pointwise by taking the complement of $x(i)$ for each index $i$. That is, $x^\complement(i) = (x(i))^\complement$ for all $i$.

Pi.compl_apply theorem

[∀ i, HasCompl (π i)] (x : ∀ i, π i) (i : ι) : xᶜ i = (x i)ᶜ

Full source

@[simp]
theorem Pi.compl_apply [∀ i, HasCompl (π i)] (x : ∀ i, π i) (i : ι) :
    xᶜ i = (x i)ᶜ :=
  rfl

Pointwise Complement Evaluation in Product Types

Informal description

For any family of types $\pi_i$ indexed by $i \in \iota$ where each $\pi_i$ has a complement operation, and for any element $x$ in the product type $\prod_{i} \pi_i$, the complement of $x$ evaluated at index $i$ is equal to the complement of $x_i$, i.e., $(x^\complement)_i = (x_i)^\complement$.

IsIrrefl.compl instance

(r) [IsIrrefl α r] : IsRefl α rᶜ

Full source

instance IsIrrefl.compl (r) [IsIrrefl α r] : IsRefl α rᶜ :=
  ⟨@irrefl α r _⟩

Complement of Irreflexive Relation is Reflexive

Informal description

For any type $\alpha$ with an irreflexive relation $r$, the complement relation $r^\mathsf{c}$ is reflexive.

IsRefl.compl instance

(r) [IsRefl α r] : IsIrrefl α rᶜ

Full source

instance IsRefl.compl (r) [IsRefl α r] : IsIrrefl α rᶜ :=
  ⟨fun a ↦ not_not_intro (refl a)⟩

Complement of Reflexive Relation is Irreflexive

Informal description

For any type $\alpha$ with a reflexive relation $r$, the complement relation $r^\mathsf{c}$ is irreflexive.

compl_lt theorem

[LinearOrder α] : (· < · : α → α → _)ᶜ = (· ≥ ·)

Full source

theorem compl_lt [LinearOrder α] : (· < · : α → α → _)ᶜ = (· ≥ ·) := by ext; simp [compl]

Complement of Strict Less-Than Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the complement of the strict less-than relation $<$ is the greater-than-or-equal-to relation $\geq$. That is, $(<)^\mathsf{c} = \geq$.

compl_le theorem

[LinearOrder α] : (· ≤ · : α → α → _)ᶜ = (· > ·)

Full source

theorem compl_le [LinearOrder α] : (· ≤ · : α → α → _)ᶜ = (· > ·) := by ext; simp [compl]

Complement of $\leq$ is $>$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the complement of the less-than-or-equal-to relation $\leq$ is the strict greater-than relation $>$. That is, $(\leq)^\mathsf{c} = >$.

compl_gt theorem

[LinearOrder α] : (· > · : α → α → _)ᶜ = (· ≤ ·)

Full source

theorem compl_gt [LinearOrder α] : (· > · : α → α → _)ᶜ = (· ≤ ·) := by ext; simp [compl]

Complement of Strict Greater-Than Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the complement of the strict greater-than relation $>$ is the less-than-or-equal-to relation $\leq$. That is, $(>)^\mathsf{c} = \leq$.

compl_ge theorem

[LinearOrder α] : (· ≥ · : α → α → _)ᶜ = (· < ·)

Full source

theorem compl_ge [LinearOrder α] : (· ≥ · : α → α → _)ᶜ = (· < ·) := by ext; simp [compl]

Complement of Greater-Than-Or-Equal Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the complement of the greater-than-or-equal-to relation $\geq$ is the strict less-than relation $<$. That is, $(\geq)^\mathsf{c} = <$.

Ne.instIsEquiv_compl instance

: IsEquiv α (· ≠ ·)ᶜ

Full source

instance Ne.instIsEquiv_compl : IsEquiv α (· ≠ ·)ᶜ := by
  convert eq_isEquiv α
  simp [compl]

Complement of Inequality is an Equivalence Relation

Informal description

The complement of the inequality relation $\neq$ on a type $\alpha$ is an equivalence relation.

Pi.hasLe instance

[∀ i, LE (π i)] : LE (∀ i, π i)

Full source

instance Pi.hasLe [∀ i, LE (π i)] :
    LE (∀ i, π i) where le x y := ∀ i, x i ≤ y i

Preorder on Function Spaces

Informal description

For any family of types $\pi_i$ each equipped with a preorder $\leq_i$, the function space $\forall i, \pi_i$ has a canonical preorder structure where $f \leq g$ if and only if $f(i) \leq_i g(i)$ for all $i$.

Pi.le_def theorem

[∀ i, LE (π i)] {x y : ∀ i, π i} : x ≤ y ↔ ∀ i, x i ≤ y i

Full source

theorem Pi.le_def [∀ i, LE (π i)] {x y : ∀ i, π i} :
    x ≤ y ↔ ∀ i, x i ≤ y i :=
  Iff.rfl

Pointwise Order Characterization in Function Spaces

Informal description

For any family of types $\pi_i$ each equipped with a preorder $\leq_i$, and for any two functions $x, y$ in the function space $\forall i, \pi_i$, we have $x \leq y$ if and only if $x(i) \leq_i y(i)$ for all indices $i$.

Pi.preorder instance

[∀ i, Preorder (π i)] : Preorder (∀ i, π i)

Full source

instance Pi.preorder [∀ i, Preorder (π i)] : Preorder (∀ i, π i) where
  __ := inferInstanceAs (LE (∀ i, π i))
  le_refl := fun a i ↦ le_refl (a i)
  le_trans := fun _ _ _ h₁ h₂ i ↦ le_trans (h₁ i) (h₂ i)

Preorder Structure on Function Spaces

Informal description

For any family of types $\pi_i$ each equipped with a preorder structure, the function space $\forall i, \pi_i$ has a canonical preorder structure where $f \leq g$ if and only if $f(i) \leq g(i)$ for all $i$.

Pi.lt_def theorem

[∀ i, Preorder (π i)] {x y : ∀ i, π i} : x < y ↔ x ≤ y ∧ ∃ i, x i < y i

Full source

theorem Pi.lt_def [∀ i, Preorder (π i)] {x y : ∀ i, π i} :
    x < y ↔ x ≤ y ∧ ∃ i, x i < y i := by
  simp +contextual [lt_iff_le_not_le, Pi.le_def]

Pointwise Strict Order Characterization in Function Spaces

Informal description

For a family of types $\pi_i$ each equipped with a preorder, and for any two functions $x, y$ in the function space $\forall i, \pi_i$, we have $x < y$ if and only if $x \leq y$ pointwise (i.e., $x(i) \leq y(i)$ for all $i$) and there exists at least one index $i$ such that $x(i) < y(i)$.

Pi.partialOrder instance

[∀ i, PartialOrder (π i)] : PartialOrder (∀ i, π i)

Full source

instance Pi.partialOrder [∀ i, PartialOrder (π i)] : PartialOrder (∀ i, π i) where
  __ := Pi.preorder
  le_antisymm := fun _ _ h1 h2 ↦ funext fun b ↦ (h1 b).antisymm (h2 b)

Partial Order Structure on Function Spaces

Informal description

For any family of types $\pi_i$ each equipped with a partial order structure, the function space $\forall i, \pi_i$ has a canonical partial order structure where $f \leq g$ if and only if $f(i) \leq g(i)$ for all $i$.

Sum.elim_le_elim_iff theorem

 {u₁ v₁ : α₁ → β} {u₂ v₂ : α₂ → β} : Sum.elim u₁ u₂ ≤ Sum.elim v₁ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂

Full source

@[simp]
lemma elim_le_elim_iff {u₁ v₁ : α₁ → β} {u₂ v₂ : α₂ → β} :
    Sum.elimSum.elim u₁ u₂ ≤ Sum.elim v₁ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂ :=
  Sum.forall

Pointwise Inequality of Sum-Eliminated Functions

Informal description

For any functions $u_1, v_1 : \alpha_1 \to \beta$ and $u_2, v_2 : \alpha_2 \to \beta$, the pointwise inequality $\text{Sum.elim}\, u_1\, u_2 \leq \text{Sum.elim}\, v_1\, v_2$ holds if and only if both $u_1 \leq v_1$ and $u_2 \leq v_2$ hold pointwise.

Sum.const_le_elim_iff theorem

 {b : β} {v₁ : α₁ → β} {v₂ : α₂ → β} :
  Function.const _ b ≤ Sum.elim v₁ v₂ ↔ Function.const _ b ≤ v₁ ∧ Function.const _ b ≤ v₂

Full source

lemma const_le_elim_iff {b : β} {v₁ : α₁ → β} {v₂ : α₂ → β} :
    Function.constFunction.const _ b ≤ Sum.elim v₁ v₂ ↔ Function.const _ b ≤ v₁ ∧ Function.const _ b ≤ v₂ :=
  elim_const_const b ▸ elim_le_elim_iff ..

Pointwise Comparison of Constant and Sum-Eliminated Functions: $\text{const}\, b \leq \text{Sum.elim}\, v_1\, v_2$ iff $\text{const}\, b \leq v_1$ and $\text{const}\, b \leq v_2$

Informal description

For any element $b$ in a type $\beta$ with a preorder, and any functions $v_1 : \alpha_1 \to \beta$ and $v_2 : \alpha_2 \to \beta$, the constant function $\text{const}\, b$ is pointwise less than or equal to the sum-eliminated function $\text{Sum.elim}\, v_1\, v_2$ if and only if $\text{const}\, b$ is pointwise less than or equal to both $v_1$ and $v_2$.

Sum.elim_le_const_iff theorem

 {b : β} {u₁ : α₁ → β} {u₂ : α₂ → β} :
  Sum.elim u₁ u₂ ≤ Function.const _ b ↔ u₁ ≤ Function.const _ b ∧ u₂ ≤ Function.const _ b

Full source

lemma elim_le_const_iff {b : β} {u₁ : α₁ → β} {u₂ : α₂ → β} :
    Sum.elimSum.elim u₁ u₂ ≤ Function.const _ b ↔ u₁ ≤ Function.const _ b ∧ u₂ ≤ Function.const _ b :=
  elim_const_const b ▸ elim_le_elim_iff ..

Pointwise Comparison of Sum-Eliminated and Constant Functions: $\text{Sum.elim}\, u_1\, u_2 \leq \text{const}\, b$ iff $u_1 \leq \text{const}\, b$ and $u_2 \leq \text{const}\, b$

Informal description

For any element $b$ in a type $\beta$ with a preorder, and any functions $u_1 : \alpha_1 \to \beta$ and $u_2 : \alpha_2 \to \beta$, the sum-eliminated function $\text{Sum.elim}\, u_1\, u_2$ is pointwise less than or equal to the constant function $\text{const}\, b$ if and only if both $u_1 \leq \text{const}\, b$ and $u_2 \leq \text{const}\, b$ hold pointwise.

StrongLT definition

[∀ i, LT (π i)] (a b : ∀ i, π i) : Prop

Full source

/-- A function `a` is strongly less than a function `b` if `a i < b i` for all `i`. -/
def StrongLT [∀ i, LT (π i)] (a b : ∀ i, π i) : Prop :=
  ∀ i, a i < b i

Strongly less than relation for functions

Informal description

Given a family of types $\{\pi_i\}_{i \in I}$ each equipped with a less-than relation $<$, the relation $\text{StrongLT}$ between two functions $a, b \in \prod_{i \in I} \pi_i$ is defined by $a \text{StrongLT} b$ if and only if $a(i) < b(i)$ for every $i \in I$.

le_of_strongLT theorem

(h : a ≺ b) : a ≤ b

Full source

theorem le_of_strongLT (h : a ≺ b) : a ≤ b := fun _ ↦ (h _).le

Pointwise Strong Inequality Implies Pointwise Weak Inequality

Informal description

For any two functions $a, b \in \prod_{i \in I} \pi_i$ where each $\pi_i$ is equipped with a preorder $\leq_i$, if $a$ is strongly less than $b$ (i.e., $a(i) < b(i)$ for all $i \in I$), then $a$ is less than or equal to $b$ in the pointwise order (i.e., $a(i) \leq_i b(i)$ for all $i \in I$).

lt_of_strongLT theorem

[Nonempty ι] (h : a ≺ b) : a < b

Full source

theorem lt_of_strongLT [Nonempty ι] (h : a ≺ b) : a < b := by
  inhabit ι
  exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

Strong Pointwise Inequality Implies Strict Pointwise Inequality for Nonempty Domains

Informal description

For a nonempty index set $I$ and functions $a, b \in \prod_{i \in I} \pi_i$ where each $\pi_i$ is equipped with a preorder, if $a$ is strongly less than $b$ (i.e., $a(i) < b(i)$ for all $i \in I$), then $a$ is strictly less than $b$ in the pointwise order (i.e., $a \leq b$ and there exists some $i \in I$ such that $a(i) < b(i)$).

strongLT_of_strongLT_of_le theorem

(hab : a ≺ b) (hbc : b ≤ c) : a ≺ c

Full source

theorem strongLT_of_strongLT_of_le (hab : a ≺ b) (hbc : b ≤ c) : a ≺ c := fun _ ↦
  (hab _).trans_le <| hbc _

Strongly Less-Than is Preserved Under Right Composition with Less-Than-or-Equal

Informal description

For functions $a, b, c$ in a product space $\prod_{i \in I} \pi_i$ where each $\pi_i$ is equipped with a preorder $\leq_i$, if $a$ is strongly less than $b$ (i.e., $a(i) < b(i)$ for all $i \in I$) and $b$ is less than or equal to $c$ (i.e., $b(i) \leq_i c(i)$ for all $i \in I$), then $a$ is strongly less than $c$ (i.e., $a(i) < c(i)$ for all $i \in I$).

strongLT_of_le_of_strongLT theorem

(hab : a ≤ b) (hbc : b ≺ c) : a ≺ c

Full source

theorem strongLT_of_le_of_strongLT (hab : a ≤ b) (hbc : b ≺ c) : a ≺ c := fun _ ↦
  (hab _).trans_lt <| hbc _

Pointwise Order and Strong Inequality Imply Strong Inequality

Informal description

For functions $a, b, c$ in a product space $\prod_{i \in I} \pi_i$ where each $\pi_i$ has a preorder $\leq_i$, if $a \leq b$ (pointwise) and $b \text{StrongLT} c$ (i.e., $b(i) < c(i)$ for all $i \in I$), then $a \text{StrongLT} c$ (i.e., $a(i) < c(i)$ for all $i \in I$).

le_update_iff theorem

: x ≤ Function.update y i a ↔ x i ≤ a ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j

Full source

theorem le_update_iff : x ≤ Function.update y i a ↔ x i ≤ a ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j :=
  Function.forall_update_iff _ fun j z ↦ x j ≤ z

Pointwise Order Characterization of Function Update

Informal description

For functions $x, y$ in a product space $\prod_{i \in I} \pi_i$ where each $\pi_i$ is equipped with a preorder $\leq_i$, an index $i \in I$, and a value $a \in \pi_i$, the following equivalence holds: \[ x \leq \text{update } y \, i \, a \quad \leftrightarrow \quad x(i) \leq a \land (\forall j \neq i, x(j) \leq y(j)). \]

update_le_iff theorem

: Function.update x i a ≤ y ↔ a ≤ y i ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j

Full source

theorem update_le_iff : Function.updateFunction.update x i a ≤ y ↔ a ≤ y i ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j :=
  Function.forall_update_iff _ fun j z ↦ z ≤ y j

Inequality Characterization of Function Update: $\text{update } x \, i \, a \leq y \leftrightarrow (a \leq y(i)) \land (\forall j \neq i, x(j) \leq y(j))$

Informal description

For functions $x, y$ in a product space $\prod_{i \in I} \pi_i$ where each $\pi_i$ is equipped with a preorder $\leq_i$, an index $i \in I$, and a value $a \in \pi_i$, the following equivalence holds: \[ \text{update } x \, i \, a \leq y \quad \leftrightarrow \quad a \leq y(i) \land (\forall j \neq i, x(j) \leq y(j)). \]

update_le_update_iff theorem

: Function.update x i a ≤ Function.update y i b ↔ a ≤ b ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j

Full source

theorem update_le_update_iff :
    Function.updateFunction.update x i a ≤ Function.update y i b ↔ a ≤ b ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j := by
  simp +contextual [update_le_iff]

Inequality of Function Updates: $\text{update } x \, i \, a \leq \text{update } y \, i \, b \leftrightarrow (a \leq b) \land (\forall j \neq i, x(j) \leq y(j))$

Informal description

For any functions $x$ and $y$, index $i$, and values $a$ and $b$, the updated function $\text{update } x \, i \, a$ is less than or equal to $\text{update } y \, i \, b$ if and only if $a \leq b$ and for all indices $j \neq i$, $x(j) \leq y(j)$.

update_le_update_iff' theorem

: update x i a ≤ update x i b ↔ a ≤ b

Full source

@[simp]
theorem update_le_update_iff' : updateupdate x i a ≤ update x i b ↔ a ≤ b := by
  simp [update_le_update_iff]

Inequality of Function Updates at Same Index: $\text{update } x \, i \, a \leq \text{update } x \, i \, b \leftrightarrow a \leq b$

Informal description

For any function $x$, index $i$, and values $a$ and $b$, the updated function $\text{update } x \, i \, a$ is less than or equal to $\text{update } x \, i \, b$ if and only if $a \leq b$.

update_lt_update_iff theorem

: update x i a < update x i b ↔ a < b

Full source

@[simp]
theorem update_lt_update_iff : updateupdate x i a < update x i b ↔ a < b :=
  lt_iff_lt_of_le_iff_le' update_le_update_iff' update_le_update_iff'

Strict Inequality of Function Updates at Same Index: $\text{update } x \, i \, a < \text{update } x \, i \, b \leftrightarrow a < b$

Informal description

For any function $x$, index $i$, and values $a$ and $b$, the updated function $\text{update } x \, i \, a$ is strictly less than $\text{update } x \, i \, b$ if and only if $a < b$.

le_update_self_iff theorem

: x ≤ update x i a ↔ x i ≤ a

Full source

@[simp]
theorem le_update_self_iff : x ≤ update x i a ↔ x i ≤ a := by simp [le_update_iff]

Inequality Between Function and Its Update: $x \leq \text{update } x \, i \, a \leftrightarrow x(i) \leq a$

Informal description

For any function $x$, index $i$, and value $a$, the inequality $x \leq \text{update } x \, i \, a$ holds if and only if $x(i) \leq a$.

update_le_self_iff theorem

: update x i a ≤ x ↔ a ≤ x i

Full source

@[simp]
theorem update_le_self_iff : updateupdate x i a ≤ x ↔ a ≤ x i := by simp [update_le_iff]

Inequality for Function Update at a Point: $\text{update } x \, i \, a \leq x \leftrightarrow a \leq x(i)$

Informal description

For a function $x$ and an index $i$, the updated function $\text{update } x \, i \, a$ is less than or equal to $x$ if and only if $a \leq x(i)$.

lt_update_self_iff theorem

: x < update x i a ↔ x i < a

Full source

@[simp]
theorem lt_update_self_iff : x < update x i a ↔ x i < a := by simp [lt_iff_le_not_le]

Strict Inequality Between Function and Its Update: $x < \text{update } x \, i \, a \leftrightarrow x(i) < a$

Informal description

For any function $x$, index $i$, and value $a$, the strict inequality $x < \text{update } x \, i \, a$ holds if and only if $x(i) < a$.

update_lt_self_iff theorem

: update x i a < x ↔ a < x i

Full source

@[simp]
theorem update_lt_self_iff : updateupdate x i a < x ↔ a < x i := by simp [lt_iff_le_not_le]

Strict Inequality for Function Update at a Point: $\text{update } x \, i \, a < x \leftrightarrow a < x(i)$

Informal description

For a function $x$ and an index $i$, the updated function $\text{update } x \, i \, a$ is strictly less than $x$ if and only if $a < x(i)$.

Pi.sdiff instance

[∀ i, SDiff (π i)] : SDiff (∀ i, π i)

Full source

instance Pi.sdiff [∀ i, SDiff (π i)] : SDiff (∀ i, π i) :=
  ⟨fun x y i ↦ x i \ y i⟩

Pointwise Set Difference on Product Types

Informal description

For any family of types $\pi_i$ each equipped with a set difference operation, the product type $\forall i, \pi_i$ inherits a set difference operation defined pointwise.

Pi.sdiff_def theorem

[∀ i, SDiff (π i)] (x y : ∀ i, π i) : x \ y = fun i ↦ x i \ y i

Full source

theorem Pi.sdiff_def [∀ i, SDiff (π i)] (x y : ∀ i, π i) :
    x \ y = fun i ↦ x i \ y i :=
  rfl

Pointwise Definition of Set Difference on Product Types

Informal description

For any family of types $\pi_i$ indexed by $i \in \iota$ where each $\pi_i$ is equipped with a set difference operation $\setminus$, the set difference operation on the product type $\forall i, \pi_i$ is defined pointwise as $(x \setminus y)(i) = x(i) \setminus y(i)$ for all $i \in \iota$.

Pi.sdiff_apply theorem

[∀ i, SDiff (π i)] (x y : ∀ i, π i) (i : ι) : (x \ y) i = x i \ y i

Full source

@[simp]
theorem Pi.sdiff_apply [∀ i, SDiff (π i)] (x y : ∀ i, π i) (i : ι) :
    (x \ y) i = x i \ y i :=
  rfl

Pointwise Set Difference Evaluation: $(x \setminus y)_i = x_i \setminus y_i$

Informal description

For any family of types $\pi_i$ each equipped with a set difference operation, and for any elements $x, y$ in the product type $\forall i, \pi_i$, the set difference operation applied pointwise at index $i$ satisfies $(x \setminus y)_i = x_i \setminus y_i$.

Function.const_le_const theorem

: const β a ≤ const β b ↔ a ≤ b

Full source

@[simp]
theorem const_le_const : constconst β a ≤ const β b ↔ a ≤ b := by simp [Pi.le_def]

Order Comparison of Constant Functions

Informal description

For any type $\beta$ with a preorder and elements $a, b \in \beta$, the constant functions $\text{const}_\beta a$ and $\text{const}_\beta b$ satisfy $\text{const}_\beta a \leq \text{const}_\beta b$ if and only if $a \leq b$.

Function.const_lt_const theorem

: const β a < const β b ↔ a < b

Full source

@[simp]
theorem const_lt_const : constconst β a < const β b ↔ a < b := by simpa [Pi.lt_def] using le_of_lt

Strict Order Comparison of Constant Functions: $\text{const}_\beta a < \text{const}_\beta b \leftrightarrow a < b$

Informal description

For any type $\beta$ equipped with a preorder and elements $a, b \in \beta$, the constant functions $\text{const}_\beta a$ and $\text{const}_\beta b$ satisfy $\text{const}_\beta a < \text{const}_\beta b$ if and only if $a < b$.

Preorder.lift abbrev

[Preorder β] (f : α → β) : Preorder α

Full source

/-- Transfer a `Preorder` on `β` to a `Preorder` on `α` using a function `f : α → β`.
See note [reducible non-instances]. -/
abbrev Preorder.lift [Preorder β] (f : α → β) : Preorder α where
  le x y := f x ≤ f y
  le_refl _ := le_rfl
  le_trans _ _ _ := _root_.le_trans
  lt x y := f x < f y
  lt_iff_le_not_le _ _ := _root_.lt_iff_le_not_le

Lifting a Preorder via a Function

Informal description

Given a preorder on a type $\beta$ and a function $f : \alpha \to \beta$, we can define a preorder on $\alpha$ by setting $a \leq b$ if and only if $f(a) \leq f(b)$ for all $a, b \in \alpha$.

PartialOrder.lift abbrev

[PartialOrder β] (f : α → β) (inj : Injective f) : PartialOrder α

Full source

/-- Transfer a `PartialOrder` on `β` to a `PartialOrder` on `α` using an injective
function `f : α → β`. See note [reducible non-instances]. -/
abbrev PartialOrder.lift [PartialOrder β] (f : α → β) (inj : Injective f) : PartialOrder α :=
  { Preorder.lift f with le_antisymm := fun _ _ h₁ h₂ ↦ inj (h₁.antisymm h₂) }

Lifting a Partial Order via an Injective Function

Informal description

Given a partial order on a type $\beta$ and an injective function $f : \alpha \to \beta$, we can define a partial order on $\alpha$ by setting $a \leq b$ if and only if $f(a) \leq f(b)$ for all $a, b \in \alpha$.

compare_of_injective_eq_compareOfLessAndEq theorem

 (a b : α) [LinearOrder β] [DecidableEq α] (f : α → β) (inj : Injective f)
  [Decidable (LT.lt (self := PartialOrder.lift f inj |>.toLT) a b)] :
  compare (f a) (f b) = @compareOfLessAndEq _ a b (PartialOrder.lift f inj |>.toLT) _ _

Full source

theorem compare_of_injective_eq_compareOfLessAndEq (a b : α) [LinearOrder β]
    [DecidableEq α] (f : α → β) (inj : Injective f)
    [Decidable (LT.lt (self := PartialOrder.lift f inj |>.toLT) a b)] :
    compare (f a) (f b) =
      @compareOfLessAndEq _ a b (PartialOrder.lift f inj |>.toLT) _ _ := by
  have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
  simp only [h, compareOfLessAndEq]
  split_ifs <;> try (first | rfl | contradiction)
  · have : ¬ f a = f b := by rename_i h; exact inj.ne h
    contradiction
  · have : f a = f b := by rename_i h; exact congrArg f h
    contradiction

Comparison Preservation under Injective Order Lifting

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a linear order, and let $f : \alpha \to \beta$ be an injective function. For any $a, b \in \alpha$, the comparison of $f(a)$ and $f(b)$ under the linear order on $\beta$ is equal to the comparison of $a$ and $b$ under the partial order on $\alpha$ lifted from $\beta$ via $f$.

LinearOrder.lift abbrev

 [LinearOrder β] [Max α] [Min α] (f : α → β) (inj : Injective f) (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y))
  (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) : LinearOrder α

Full source

/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version takes `[Max α]` and `[Min α]` as arguments, then uses
them for `max` and `min` fields. See `LinearOrder.lift'` for a version that autogenerates `min` and
`max` fields, and `LinearOrder.liftWithOrd` for one that does not auto-generate `compare`
fields. See note [reducible non-instances]. -/
abbrev LinearOrder.lift [LinearOrder β] [Max α] [Min α] (f : α → β) (inj : Injective f)
    (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
    LinearOrder α :=
  letI instOrdα : Ord α := ⟨fun a b ↦ compare (f a) (f b)⟩
  letI decidableLE := fun x y ↦ (inferInstance : Decidable (f x ≤ f y))
  letI decidableLT := fun x y ↦ (inferInstance : Decidable (f x < f y))
  letI decidableEq := fun x y ↦ decidable_of_iff (f x = f y) inj.eq_iff
  { PartialOrder.lift f inj, instOrdα with
    le_total := fun x y ↦ le_total (f x) (f y)
    toDecidableLE := decidableLE
    toDecidableLT := decidableLT
    toDecidableEq := decidableEq
    min := (· ⊓ ·)
    max := (· ⊔ ·)
    min_def := by
      intros x y
      apply inj
      rw [apply_ite f]
      exact (hinf _ _).trans (min_def _ _)
    max_def := by
      intros x y
      apply inj
      rw [apply_ite f]
      exact (hsup _ _).trans (max_def _ _)
    compare_eq_compareOfLessAndEq := fun a b ↦
      compare_of_injective_eq_compareOfLessAndEq a b f inj }

Lifting a Linear Order via an Injective Function Preserving Max and Min

Informal description

Given a linear order on a type $\beta$, an injective function $f : \alpha \to \beta$, and operations $\sqcup$ and $\sqcap$ on $\alpha$ that satisfy $f(x \sqcup y) = \max(f(x), f(y))$ and $f(x \sqcap y) = \min(f(x), f(y))$ for all $x, y \in \alpha$, we can define a linear order on $\alpha$ by setting $a \leq b$ if and only if $f(a) \leq f(b)$ for all $a, b \in \alpha$.

LinearOrder.lift' abbrev

[LinearOrder β] (f : α → β) (inj : Injective f) : LinearOrder α

Full source

/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version autogenerates `min` and `max` fields. See `LinearOrder.lift`
for a version that takes `[Max α]` and `[Min α]`, then uses them as `max` and `min`. See
`LinearOrder.liftWithOrd'` for a version which does not auto-generate `compare` fields.
See note [reducible non-instances]. -/
abbrev LinearOrder.lift' [LinearOrder β] (f : α → β) (inj : Injective f) : LinearOrder α :=
  @LinearOrder.lift α β _ ⟨fun x y ↦ if f x ≤ f y then y else x⟩
    ⟨fun x y ↦ if f x ≤ f y then x else y⟩ f inj
    (fun _ _ ↦ (apply_ite f _ _ _).trans (max_def _ _).symm) fun _ _ ↦
    (apply_ite f _ _ _).trans (min_def _ _).symm

Lifting a Linear Order via an Injective Function (Autogenerated Min/Max)

Informal description

Given a linear order on a type $\beta$ and an injective function $f \colon \alpha \to \beta$, we can define a linear order on $\alpha$ by setting $a \leq b$ if and only if $f(a) \leq f(b)$ for all $a, b \in \alpha$. This version automatically generates the minimum and maximum operations on $\alpha$.

LinearOrder.liftWithOrd abbrev

 [LinearOrder β] [Max α] [Min α] [Ord α] (f : α → β) (inj : Injective f) (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y))
  (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) (compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α

Full source

/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version takes `[Max α]` and `[Min α]` as arguments, then uses
them for `max` and `min` fields. It also takes `[Ord α]` as an argument and uses them for `compare`
fields. See `LinearOrder.lift` for a version that autogenerates `compare` fields, and
`LinearOrder.liftWithOrd'` for one that auto-generates `min` and `max` fields.
fields. See note [reducible non-instances]. -/
abbrev LinearOrder.liftWithOrd [LinearOrder β] [Max α] [Min α] [Ord α] (f : α → β)
    (inj : Injective f) (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y))
    (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y))
    (compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α :=
  letI decidableLE := fun x y ↦ (inferInstance : Decidable (f x ≤ f y))
  letI decidableLT := fun x y ↦ (inferInstance : Decidable (f x < f y))
  letI decidableEq := fun x y ↦ decidable_of_iff (f x = f y) inj.eq_iff
  { PartialOrder.lift f inj with
    le_total := fun x y ↦ le_total (f x) (f y)
    toDecidableLE := decidableLE
    toDecidableLT := decidableLT
    toDecidableEq := decidableEq
    min := (· ⊓ ·)
    max := (· ⊔ ·)
    min_def := by
      intros x y
      apply inj
      rw [apply_ite f]
      exact (hinf _ _).trans (min_def _ _)
    max_def := by
      intros x y
      apply inj
      rw [apply_ite f]
      exact (hsup _ _).trans (max_def _ _)
    compare_eq_compareOfLessAndEq := fun a b ↦
      (compare_f a b).trans <| compare_of_injective_eq_compareOfLessAndEq a b f inj }

Lifting a Linear Order via an Injective Function Preserving Max, Min, and Compare

Informal description

Given a linear order on a type $\beta$, an injective function $f \colon \alpha \to \beta$, and operations $\sqcup$ (maximum) and $\sqcap$ (minimum) on $\alpha$ that satisfy $f(x \sqcup y) = \max(f(x), f(y))$ and $f(x \sqcap y) = \min(f(x), f(y))$ for all $x, y \in \alpha$, along with a comparison function on $\alpha$ that satisfies $\text{compare}(a, b) = \text{compare}(f(a), f(b))$ for all $a, b \in \alpha$, we can define a linear order on $\alpha$ by setting $a \leq b$ if and only if $f(a) \leq f(b)$ for all $a, b \in \alpha$.

LinearOrder.liftWithOrd' abbrev

 [LinearOrder β] [Ord α] (f : α → β) (inj : Injective f) (compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) :
  LinearOrder α

Full source

/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version auto-generates `min` and `max` fields. It also takes `[Ord α]`
as an argument and uses them for `compare` fields. See `LinearOrder.lift` for a version that
autogenerates `compare` fields, and `LinearOrder.liftWithOrd` for one that doesn't auto-generate
`min` and `max` fields. fields. See note [reducible non-instances]. -/
abbrev LinearOrder.liftWithOrd' [LinearOrder β] [Ord α] (f : α → β)
    (inj : Injective f)
    (compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α :=
  @LinearOrder.liftWithOrd α β _ ⟨fun x y ↦ if f x ≤ f y then y else x⟩
    ⟨fun x y ↦ if f x ≤ f y then x else y⟩ _ f inj
    (fun _ _ ↦ (apply_ite f _ _ _).trans (max_def _ _).symm)
    (fun _ _ ↦ (apply_ite f _ _ _).trans (min_def _ _).symm)
    compare_f

Lifting a Linear Order via an Injective Function Preserving Compare

Informal description

Given a linear order on a type $\beta$, an injective function $f \colon \alpha \to \beta$, and a comparison function on $\alpha$ that satisfies $\text{compare}(a, b) = \text{compare}(f(a), f(b))$ for all $a, b \in \alpha$, we can define a linear order on $\alpha$ by setting $a \leq b$ if and only if $f(a) \leq f(b)$ for all $a, b \in \alpha$.

Subtype.le instance

[LE α] {p : α → Prop} : LE (Subtype p)

Full source

instance le [LE α] {p : α → Prop} : LE (Subtype p) :=
  ⟨fun x y ↦ (x : α) ≤ y⟩

Preorder on Subtypes

Informal description

For any type $\alpha$ with a preorder (given by a relation $\leq$) and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a preorder structure where $x \leq y$ is defined as in $\alpha$.

Subtype.lt instance

[LT α] {p : α → Prop} : LT (Subtype p)

Full source

instance lt [LT α] {p : α → Prop} : LT (Subtype p) :=
  ⟨fun x y ↦ (x : α) < y⟩

Strict Order on Subtypes

Informal description

For any type $\alpha$ with a strict order relation $<$ and a predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a strict order relation from $\alpha$, where $x < y$ in the subtype if and only if $x < y$ in $\alpha$.

Subtype.mk_le_mk theorem

[LE α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} : (⟨x, hx⟩ : Subtype p) ≤ ⟨y, hy⟩ ↔ x ≤ y

Full source

@[simp]
theorem mk_le_mk [LE α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
    (⟨x, hx⟩ : Subtype p) ≤ ⟨y, hy⟩ ↔ x ≤ y :=
  Iff.rfl

Subtype Inequality Equivalence: $\langle x, hx \rangle \leq \langle y, hy \rangle \leftrightarrow x \leq y$

Informal description

For any type $\alpha$ equipped with a preorder (given by a relation $\leq$) and any predicate $p$ on $\alpha$, given elements $x, y \in \alpha$ with proofs $hx : p(x)$ and $hy : p(y)$, the inequality $\langle x, hx \rangle \leq \langle y, hy \rangle$ holds in the subtype $\{x \in \alpha \mid p(x)\}$ if and only if $x \leq y$ holds in $\alpha$.

Subtype.mk_lt_mk theorem

[LT α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} : (⟨x, hx⟩ : Subtype p) < ⟨y, hy⟩ ↔ x < y

Full source

@[simp]
theorem mk_lt_mk [LT α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
    (⟨x, hx⟩ : Subtype p) < ⟨y, hy⟩ ↔ x < y :=
  Iff.rfl

Subtype Strict Order Correspondence: $\langle x, hx \rangle < \langle y, hy \rangle \leftrightarrow x < y$

Informal description

For any type $\alpha$ with a strict order relation $<$, a predicate $p$ on $\alpha$, and elements $x, y \in \alpha$ satisfying $p(x)$ and $p(y)$ respectively, the inequality $\langle x, hx \rangle < \langle y, hy \rangle$ holds in the subtype $\{x \in \alpha \mid p(x)\}$ if and only if $x < y$ holds in $\alpha$.

Subtype.coe_le_coe theorem

[LE α] {p : α → Prop} {x y : Subtype p} : (x : α) ≤ y ↔ x ≤ y

Full source

@[simp, norm_cast]
theorem coe_le_coe [LE α] {p : α → Prop} {x y : Subtype p} : (x : α) ≤ y ↔ x ≤ y :=
  Iff.rfl

Subtype Inequality Preservation Under Coercion

Informal description

For any type $\alpha$ with a preorder $\leq$ and any predicate $p$ on $\alpha$, given two elements $x$ and $y$ in the subtype $\{a \in \alpha \mid p(a)\}$, the inequality $x \leq y$ holds in the subtype if and only if the inequality $x \leq y$ holds in $\alpha$.

Subtype.coe_lt_coe theorem

[LT α] {p : α → Prop} {x y : Subtype p} : (x : α) < y ↔ x < y

Full source

@[simp, norm_cast]
theorem coe_lt_coe [LT α] {p : α → Prop} {x y : Subtype p} : (x : α) < y ↔ x < y :=
  Iff.rfl

Subtype Strict Order Preservation: $x < y$ in Subtype iff $x < y$ in $\alpha$

Informal description

For any type $\alpha$ with a strict order relation $<$ and a predicate $p$ on $\alpha$, given two elements $x$ and $y$ of the subtype $\{a \in \alpha \mid p(a)\}$, the inequality $x < y$ holds in the subtype if and only if the inequality $x < y$ holds in $\alpha$ when viewed as elements of $\alpha$.

Subtype.preorder instance

[Preorder α] (p : α → Prop) : Preorder (Subtype p)

Full source

instance preorder [Preorder α] (p : α → Prop) : Preorder (Subtype p) :=
  Preorder.lift (fun (a : Subtype p) ↦ (a : α))

Preorder Structure on Subtypes

Informal description

For any preorder on a type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a preorder structure from $\alpha$, where the order relation is defined by restricting the original order relation on $\alpha$ to the subtype.

Subtype.partialOrder instance

[PartialOrder α] (p : α → Prop) : PartialOrder (Subtype p)

Full source

instance partialOrder [PartialOrder α] (p : α → Prop) : PartialOrder (Subtype p) :=
  PartialOrder.lift (fun (a : Subtype p) ↦ (a : α)) Subtype.coe_injective

Partial Order Structure on Subtypes

Informal description

For any partial order on a type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a partial order structure from $\alpha$, where the order relation is defined by restricting the original order relation on $\alpha$ to the subtype.

Subtype.decidableLE instance

[Preorder α] [h : DecidableLE α] {p : α → Prop} : DecidableLE (Subtype p)

Full source

instance decidableLE [Preorder α] [h : DecidableLE α] {p : α → Prop} :
    DecidableLE (Subtype p) := fun a b ↦ h a b

Decidable Preorder on Subtypes

Informal description

For any preorder $\alpha$ with a decidable $\leq$ relation and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a decidable $\leq$ relation.

Subtype.decidableLT instance

[Preorder α] [h : DecidableLT α] {p : α → Prop} : DecidableLT (Subtype p)

Full source

instance decidableLT [Preorder α] [h : DecidableLT α] {p : α → Prop} :
    DecidableLT (Subtype p) := fun a b ↦ h a b

Decidable Strict Order on Subtypes

Informal description

For any preordered type $\alpha$ with a decidable strict order relation $<$ and a predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a decidable strict order relation from $\alpha$.

Subtype.instLinearOrder instance

[LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p)

Full source

/-- A subtype of a linear order is a linear order. We explicitly give the proofs of decidable
equality and decidable order in order to ensure the decidability instances are all definitionally
equal. -/
instance instLinearOrder [LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p) :=
  @LinearOrder.lift (Subtype p) _ _ ⟨fun x y ↦ ⟨max x y, max_rec' _ x.2 y.2⟩⟩
    ⟨fun x y ↦ ⟨min x y, min_rec' _ x.2 y.2⟩⟩ (fun (a : Subtype p) ↦ (a : α))
    Subtype.coe_injective (fun _ _ ↦ rfl) fun _ _ ↦
    rfl

Subtype of a Linear Order is a Linear Order

Informal description

For any linearly ordered type $\alpha$ and predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a linear order structure from $\alpha$.

Prod.instLE_mathlib instance

: LE (α × β)

Full source

instance : LE (α × β) where le p q := p.1 ≤ q.1 ∧ p.2 ≤ q.2

Pointwise Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ with a preorder structure, the product type $\alpha \times \beta$ is equipped with a canonical preorder structure where $(x_1, x_2) \leq (y_1, y_2)$ if and only if $x_1 \leq y_1$ and $x_2 \leq y_2$.

Prod.instDecidableLE instance

[Decidable (x.1 ≤ y.1)] [Decidable (x.2 ≤ y.2)] : Decidable (x ≤ y)

Full source

instance instDecidableLE [Decidable (x.1 ≤ y.1)] [Decidable (x.2 ≤ y.2)] : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.1 ≤ y.1 ∧ x.2 ≤ y.2))

Decidability of Pointwise Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ with decidable preorders, the product type $\alpha \times \beta$ has a decidable preorder structure where $(x_1, x_2) \leq (y_1, y_2)$ is decidable if and only if both $x_1 \leq y_1$ and $x_2 \leq y_2$ are decidable.

Prod.le_def theorem

: x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2

Full source

lemma le_def : x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2 := .rfl

Pointwise Order Characterization in Product Types

Informal description

For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product type $\alpha \times \beta$ with preorders on $\alpha$ and $\beta$, the inequality $x \leq y$ holds if and only if both $x_1 \leq y_1$ in $\alpha$ and $x_2 \leq y_2$ in $\beta$ hold.

Prod.mk_le_mk theorem

: (a₁, b₁) ≤ (a₂, b₂) ↔ a₁ ≤ a₂ ∧ b₁ ≤ b₂

Full source

@[simp] lemma mk_le_mk : (a₁, b₁)(a₁, b₁) ≤ (a₂, b₂) ↔ a₁ ≤ a₂ ∧ b₁ ≤ b₂ := .rfl

Pointwise Order Characterization in Product Types

Informal description

For elements $(a_1, b_1)$ and $(a_2, b_2)$ in the product type $\alpha \times \beta$, the inequality $(a_1, b_1) \leq (a_2, b_2)$ holds if and only if $a_1 \leq a_2$ and $b_1 \leq b_2$.

Prod.swap_le_swap theorem

: x.swap ≤ y.swap ↔ x ≤ y

Full source

@[simp] lemma swap_le_swap : x.swap ≤ y.swap ↔ x ≤ y := and_comm

Order Preservation under Component Swapping in Product Types

Informal description

For any elements $x$ and $y$ in the product type $\alpha \times \beta$, the inequality $x.\text{swap} \leq y.\text{swap}$ holds if and only if $x \leq y$. Here, $\text{swap}$ denotes the function that swaps the components of a pair, i.e., $(a, b).\text{swap} = (b, a)$.

Prod.swap_le_mk theorem

: x.swap ≤ (b, a) ↔ x ≤ (a, b)

Full source

@[simp] lemma swap_le_mk : x.swap ≤ (b, a) ↔ x ≤ (a, b) := and_comm

Order Reversal via Swap in Product Types: $x.\mathrm{swap} \leq (b, a) \leftrightarrow x \leq (a, b)$

Informal description

For any elements $x$ in $\alpha \times \beta$ and $(a, b)$ in $\alpha \times \beta$, the swapped pair $x.\mathrm{swap} \leq (b, a)$ holds if and only if $x \leq (a, b)$ holds under the pointwise order on the product type.

Prod.mk_le_swap theorem

: (b, a) ≤ x.swap ↔ (a, b) ≤ x

Full source

@[simp] lemma mk_le_swap : (b, a)(b, a) ≤ x.swap ↔ (a, b) ≤ x := and_comm

Order Reversal via Swap in Product Types

Informal description

For any elements $a, b$ in types $\alpha$ and $\beta$ respectively, and any element $x$ in $\alpha \times \beta$, the pair $(b, a)$ is less than or equal to $x.\text{swap}$ if and only if the pair $(a, b)$ is less than or equal to $x$. Here, $\text{swap}$ denotes the function that swaps the components of a pair, i.e., $(x_1, x_2).\text{swap} = (x_2, x_1)$.

Prod.instPreorder instance

: Preorder (α × β)

Full source

instance : Preorder (α × β) where
  __ := inferInstanceAs (LE (α × β))
  le_refl := fun ⟨a, b⟩ ↦ ⟨le_refl a, le_refl b⟩
  le_trans := fun ⟨_, _⟩ ⟨_, _⟩ ⟨_, _⟩ ⟨hac, hbd⟩ ⟨hce, hdf⟩ ↦ ⟨le_trans hac hce, le_trans hbd hdf⟩

Pointwise Preorder on Product Types

Informal description

For any types $\alpha$ and $\beta$ with a preorder structure, the product type $\alpha \times \beta$ is equipped with a canonical preorder structure where $(x_1, x_2) \leq (y_1, y_2)$ if and only if $x_1 \leq y_1$ and $x_2 \leq y_2$.

Prod.swap_lt_swap theorem

: x.swap < y.swap ↔ x < y

Full source

@[simp]
theorem swap_lt_swap : x.swap < y.swap ↔ x < y :=
  and_congr swap_le_swap (not_congr swap_le_swap)

Strict Order Preservation under Component Swapping in Product Types

Informal description

For any elements $x$ and $y$ in the product type $\alpha \times \beta$ with a preorder structure, the strict inequality $x.\text{swap} < y.\text{swap}$ holds if and only if $x < y$, where $\text{swap}$ denotes the function that swaps the components of a pair, i.e., $(a, b).\text{swap} = (b, a)$.

Prod.swap_lt_mk theorem

: x.swap < (b, a) ↔ x < (a, b)

Full source

@[simp] lemma swap_lt_mk : x.swap < (b, a) ↔ x < (a, b) := by rw [← swap_lt_swap]; simp

Strict Order Relation under Component Swapping in Product Types: $x.\text{swap} < (b, a) \leftrightarrow x < (a, b)$

Informal description

For any elements $x$ in the product type $\alpha \times \beta$ with a preorder structure and any elements $a \in \alpha$, $b \in \beta$, the strict inequality $x.\text{swap} < (b, a)$ holds if and only if $x < (a, b)$, where $\text{swap}$ denotes the function that swaps the components of a pair, i.e., $(a, b).\text{swap} = (b, a)$.

Prod.mk_lt_swap theorem

: (b, a) < x.swap ↔ (a, b) < x

Full source

@[simp] lemma mk_lt_swap : (b, a)(b, a) < x.swap ↔ (a, b) < x := by rw [← swap_lt_swap]; simp

Strict Order Relation under Component Swapping in Product Types: $(b, a) < x.\text{swap} \leftrightarrow (a, b) < x$

Informal description

For any elements $a \in \alpha$, $b \in \beta$, and $x \in \alpha \times \beta$ with a preorder structure, the strict inequality $(b, a) < x.\text{swap}$ holds if and only if $(a, b) < x$, where $\text{swap}$ denotes the function that swaps the components of a pair, i.e., $(a, b).\text{swap} = (b, a)$.

Prod.mk_le_mk_iff_left theorem

: (a₁, b) ≤ (a₂, b) ↔ a₁ ≤ a₂

Full source

theorem mk_le_mk_iff_left : (a₁, b)(a₁, b) ≤ (a₂, b) ↔ a₁ ≤ a₂ :=
  and_iff_left le_rfl

Comparison of First Components in Product Order

Informal description

For any elements $a₁, a₂$ of a type $\alpha$ with a preorder and any element $b$ of a type $\beta$, the pair $(a₁, b)$ is less than or equal to $(a₂, b)$ in the product order if and only if $a₁ \leq a₂$ in $\alpha$.

Prod.mk_le_mk_iff_right theorem

: (a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂

Full source

theorem mk_le_mk_iff_right : (a, b₁)(a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂ :=
  and_iff_right le_rfl

Comparison of Second Components in Product Order

Informal description

For any elements $b₁, b₂$ of a type $\beta$ with a preorder and any element $a$ of a type $\alpha$, the pair $(a, b₁)$ is less than or equal to $(a, b₂)$ in the product order if and only if $b₁ \leq b₂$ in $\beta$.

Prod.mk_lt_mk_iff_left theorem

: (a₁, b) < (a₂, b) ↔ a₁ < a₂

Full source

theorem mk_lt_mk_iff_left : (a₁, b)(a₁, b) < (a₂, b) ↔ a₁ < a₂ :=
  lt_iff_lt_of_le_iff_le' mk_le_mk_iff_left mk_le_mk_iff_left

Strict Comparison of First Components in Product Order

Informal description

For any elements $a₁, a₂$ of a type $\alpha$ with a preorder and any element $b$ of a type $\beta$, the pair $(a₁, b)$ is strictly less than $(a₂, b)$ in the product order if and only if $a₁ < a₂$ in $\alpha$.

Prod.mk_lt_mk_iff_right theorem

: (a, b₁) < (a, b₂) ↔ b₁ < b₂

Full source

theorem mk_lt_mk_iff_right : (a, b₁)(a, b₁) < (a, b₂) ↔ b₁ < b₂ :=
  lt_iff_lt_of_le_iff_le' mk_le_mk_iff_right mk_le_mk_iff_right

Strict Comparison of Second Components in Product Order

Informal description

For any elements $b₁, b₂$ of a type $\beta$ with a preorder and any element $a$ of a type $\alpha$, the pair $(a, b₁)$ is strictly less than $(a, b₂)$ in the product order if and only if $b₁ < b₂$ in $\beta$.

Prod.lt_iff theorem

: x < y ↔ x.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2

Full source

theorem lt_iff : x < y ↔ x.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2 := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · by_cases h₁ : y.1 ≤ x.1
    · exact Or.inr ⟨h.1.1, LE.le.lt_of_not_le h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
    · exact Or.inl ⟨LE.le.lt_of_not_le h.1.1 h₁, h.1.2⟩
  · rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_le h.1⟩
    · exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_le h.2⟩

Characterization of Strict Product Order via Component-wise Inequalities

Informal description

For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product of two preordered types, the strict inequality $x < y$ holds if and only if either: 1. $x_1 < y_1$ and $x_2 \leq y_2$, or 2. $x_1 \leq y_1$ and $x_2 < y_2$.

Prod.mk_lt_mk theorem

: (a₁, b₁) < (a₂, b₂) ↔ a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂

Full source

@[simp]
theorem mk_lt_mk : (a₁, b₁)(a₁, b₁) < (a₂, b₂) ↔ a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂ :=
  lt_iff

Characterization of Strict Product Order via Component-wise Inequalities

Informal description

For any elements $(a_1, b_1)$ and $(a_2, b_2)$ in the product of two preordered types, the strict inequality $(a_1, b_1) < (a_2, b_2)$ holds if and only if either: 1. $a_1 < a_2$ and $b_1 \leq b_2$, or 2. $a_1 \leq a_2$ and $b_1 < b_2$.

Prod.lt_of_lt_of_le theorem

(h₁ : x.1 < y.1) (h₂ : x.2 ≤ y.2) : x < y

Full source

protected lemma lt_of_lt_of_le (h₁ : x.1 < y.1) (h₂ : x.2 ≤ y.2) : x < y := by simp [lt_iff, *]

Strict Inequality in First Component and Weak Inequality in Second Component Implies Strict Product Order

Informal description

For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product of two preordered types, if $x_1 < y_1$ and $x_2 \leq y_2$, then $x < y$.

Prod.lt_of_le_of_lt theorem

(h₁ : x.1 ≤ y.1) (h₂ : x.2 < y.2) : x < y

Full source

protected lemma lt_of_le_of_lt (h₁ : x.1 ≤ y.1) (h₂ : x.2 < y.2) : x < y := by simp [lt_iff, *]

Weak Inequality in First Component and Strict Inequality in Second Component Implies Strict Product Order

Informal description

For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product of two preordered types, if $x_1 \leq y_1$ and $x_2 < y_2$, then $x < y$.

Prod.mk_lt_mk_of_lt_of_le theorem

(h₁ : a₁ < a₂) (h₂ : b₁ ≤ b₂) : (a₁, b₁) < (a₂, b₂)

Full source

lemma mk_lt_mk_of_lt_of_le (h₁ : a₁ < a₂) (h₂ : b₁ ≤ b₂) : (a₁, b₁) < (a₂, b₂) := by
  simp [lt_iff, *]

Strict Product Order via Component-wise Inequalities

Informal description

For any elements $a_1, a_2$ in a preorder $\alpha$ and $b_1, b_2$ in a preorder $\beta$, if $a_1 < a_2$ and $b_1 \leq b_2$, then the pair $(a_1, b_1)$ is strictly less than $(a_2, b_2)$ in the product order on $\alpha \times \beta$.

Prod.mk_lt_mk_of_le_of_lt theorem

(h₁ : a₁ ≤ a₂) (h₂ : b₁ < b₂) : (a₁, b₁) < (a₂, b₂)

Full source

lemma mk_lt_mk_of_le_of_lt (h₁ : a₁ ≤ a₂) (h₂ : b₁ < b₂) : (a₁, b₁) < (a₂, b₂) := by
  simp [lt_iff, *]

Lexicographic Order: $(a_1, b_1) < (a_2, b_2)$ when $a_1 \leq a_2$ and $b_1 < b_2$

Informal description

For any elements $a_1, a_2$ in a preorder $\alpha$ and $b_1, b_2$ in a preorder $\beta$, if $a_1 \leq a_2$ and $b_1 < b_2$, then the pair $(a_1, b_1)$ is strictly less than $(a_2, b_2)$ in the lexicographic order on $\alpha \times \beta$.

Prod.instPartialOrder instance

(α β : Type*) [PartialOrder α] [PartialOrder β] : PartialOrder (α × β)

Full source

/-- The pointwise partial order on a product.
    (The lexicographic ordering is defined in `Order.Lexicographic`, and the instances are
    available via the type synonym `α ×ₗ β = α × β`.) -/
instance instPartialOrder (α β : Type*) [PartialOrder α] [PartialOrder β] :
    PartialOrder (α × β) where
  __ := inferInstanceAs (Preorder (α × β))
  le_antisymm := fun _ _ ⟨hac, hbd⟩ ⟨hca, hdb⟩ ↦ Prod.ext (hac.antisymm hca) (hbd.antisymm hdb)

Pointwise Partial Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ with a partial order structure, the product type $\alpha \times \beta$ is equipped with a canonical partial order structure where $(x_1, x_2) \leq (y_1, y_2)$ if and only if $x_1 \leq y_1$ and $x_2 \leq y_2$.

DenselyOrdered structure

(α : Type*) [LT α]

Full source

/-- An order is dense if there is an element between any pair of distinct comparable elements. -/
class DenselyOrdered (α : Type*) [LT α] : Prop where
  /-- An order is dense if there is an element between any pair of distinct elements. -/
  dense : ∀ a₁ a₂ : α, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Dense Order

Informal description

An order on a type $\alpha$ is called *dense* if for any two elements $a_1, a_2 \in \alpha$ with $a_1 < a_2$, there exists an element $a \in \alpha$ such that $a_1 < a < a_2$.

exists_between theorem

[LT α] [DenselyOrdered α] : ∀ {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Full source

theorem exists_between [LT α] [DenselyOrdered α] : ∀ {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂ :=
  DenselyOrdered.dense _ _

Existence of Intermediate Element in Dense Order

Informal description

For any two elements $a_1$ and $a_2$ in a densely ordered type $\alpha$ with $a_1 < a_2$, there exists an element $a \in \alpha$ such that $a_1 < a < a_2$.

OrderDual.denselyOrdered instance

(α : Type*) [LT α] [h : DenselyOrdered α] : DenselyOrdered αᵒᵈ

Full source

instance OrderDual.denselyOrdered (α : Type*) [LT α] [h : DenselyOrdered α] :
    DenselyOrdered αᵒᵈ :=
  ⟨fun _ _ ha ↦ (@exists_between α _ h _ _ ha).imp fun _ ↦ And.symm⟩

Density of the Order Dual

Informal description

For any type $\alpha$ with a strict order relation $<$ that is densely ordered, the order dual $\alpha^{\text{op}}$ is also densely ordered.

denselyOrdered_orderDual theorem

[LT α] : DenselyOrdered αᵒᵈ ↔ DenselyOrdered α

Full source

@[simp]
theorem denselyOrdered_orderDual [LT α] : DenselyOrderedDenselyOrdered αᵒᵈ ↔ DenselyOrdered α :=
  ⟨by convert @OrderDual.denselyOrdered αᵒᵈ _, @OrderDual.denselyOrdered α _⟩

Density Preservation Under Order Duality: $\alpha^{\text{op}}$ Dense $\leftrightarrow$ $\alpha$ Dense

Informal description

For any type $\alpha$ with a strict order relation $<$, the order dual $\alpha^{\text{op}}$ is densely ordered if and only if $\alpha$ itself is densely ordered. In other words, the density property is preserved under order duality.

Subsingleton.instDenselyOrdered theorem

{X : Type*} [Subsingleton X] [Preorder X] : DenselyOrdered X

Full source

/-- Any ordered subsingleton is densely ordered. Not an instance to avoid a heavy subsingleton
typeclass search. -/
lemma Subsingleton.instDenselyOrdered {X : Type*} [Subsingleton X] [Preorder X] :
    DenselyOrdered X :=
  ⟨fun _ _ h ↦ (not_lt_of_subsingleton h).elim⟩

Density of Ordered Subsingletons

Informal description

For any subsingleton type $X$ with a preorder, $X$ is densely ordered. That is, for any two elements $a_1, a_2 \in X$ with $a_1 < a_2$, there exists an element $a \in X$ such that $a_1 < a < a_2$.

instDenselyOrderedProd instance

[Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α × β)

Full source

instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α × β) :=
  ⟨fun a b ↦ by
    simp_rw [Prod.lt_iff]
    rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · obtain ⟨c, ha, hb⟩ := exists_between h₁
      exact ⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h₂
      exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩⟩

Density of the Product Order on Densely Ordered Types

Informal description

For any preordered types $\alpha$ and $\beta$ that are densely ordered, the product type $\alpha \times \beta$ with the pointwise order is also densely ordered. That is, for any two pairs $(x_1, y_1) < (x_2, y_2)$ in $\alpha \times \beta$, there exists a pair $(x, y)$ such that $(x_1, y_1) < (x, y) < (x_2, y_2)$.

instDenselyOrderedForall instance

[∀ i, Preorder (π i)] [∀ i, DenselyOrdered (π i)] : DenselyOrdered (∀ i, π i)

Full source

instance [∀ i, Preorder (π i)] [∀ i, DenselyOrdered (π i)] :
    DenselyOrdered (∀ i, π i) :=
  ⟨fun a b ↦ by
    classical
      simp_rw [Pi.lt_def]
      rintro ⟨hab, i, hi⟩
      obtain ⟨c, ha, hb⟩ := exists_between hi
      exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩⟩

Density of the Pointwise Order on Function Spaces

Informal description

For any family of types $\pi_i$ each equipped with a preorder and densely ordered, the function space $\forall i, \pi_i$ is also densely ordered. That is, for any two functions $f, g$ in $\forall i, \pi_i$ with $f < g$, there exists a function $h$ such that $f < h < g$.

le_of_forall_gt_imp_ge_of_dense theorem

(h : ∀ a, a₂ < a → a₁ ≤ a) : a₁ ≤ a₂

Full source

theorem le_of_forall_gt_imp_ge_of_dense (h : ∀ a, a₂ < a → a₁ ≤ a) : a₁ ≤ a₂ :=
  le_of_not_gt fun ha ↦
    let ⟨a, ha₁, ha₂⟩ := exists_between ha
    lt_irrefl a <| lt_of_lt_of_le ‹a < a₁› (h _ ‹a₂ < a›)

Dense Order Criterion for Inequality: $\forall a>a_2, a_1 \leq a \Rightarrow a_1 \leq a_2$

Informal description

Let $\alpha$ be a densely ordered type. For any two elements $a_1, a_2 \in \alpha$, if for every $a \in \alpha$ with $a_2 < a$ we have $a_1 \leq a$, then $a_1 \leq a_2$.

forall_gt_imp_ge_iff_le_of_dense theorem

: (∀ a, a₂ < a → a₁ ≤ a) ↔ a₁ ≤ a₂

Full source

lemma forall_gt_imp_ge_iff_le_of_dense : (∀ a, a₂ < a → a₁ ≤ a) ↔ a₁ ≤ a₂ :=
  ⟨le_of_forall_gt_imp_ge_of_dense, fun ha _a ha₂ ↦ ha.trans ha₂.le⟩

Dense Order Criterion for Inequality: $\forall a>a_2, a_1 \leq a \Leftrightarrow a_1 \leq a_2$

Informal description

For any two elements $a_1, a_2$ in a densely ordered type $\alpha$, the following are equivalent: 1. For every $a \in \alpha$ with $a_2 < a$, we have $a_1 \leq a$. 2. $a_1 \leq a_2$.

le_of_forall_lt_imp_le_of_dense theorem

(h : ∀ a < a₁, a ≤ a₂) : a₁ ≤ a₂

Full source

theorem le_of_forall_lt_imp_le_of_dense (h : ∀ a < a₁, a ≤ a₂) : a₁ ≤ a₂ :=
  le_of_not_gt fun ha ↦
    let ⟨a, ha₁, ha₂⟩ := exists_between ha
    lt_irrefl a <| lt_of_le_of_lt (h _ ‹a < a₁›) ‹a₂ < a›

Dense Order Criterion for Inequality: $\forall a < a_1, a \leq a_2 \Rightarrow a_1 \leq a_2$

Informal description

Let $\alpha$ be a densely ordered type. For elements $a_1, a_2 \in \alpha$, if every element $a < a_1$ satisfies $a \leq a_2$, then $a_1 \leq a_2$.

forall_lt_imp_le_iff_le_of_dense theorem

: (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂

Full source

lemma forall_lt_imp_le_iff_le_of_dense : (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ :=
  ⟨le_of_forall_lt_imp_le_of_dense, fun ha _a ha₁ ↦ ha₁.le.trans ha⟩

Dense Order Criterion for Inequality: $\forall a < a_1, a \leq a_2 \Leftrightarrow a_1 \leq a_2$

Informal description

Let $\alpha$ be a densely ordered type. For any elements $a_1, a_2 \in \alpha$, the following are equivalent: 1. For every $a \in \alpha$ with $a < a_1$, we have $a \leq a_2$. 2. $a_1 \leq a_2$.

dense_or_discrete theorem

 [LinearOrder α] (a₁ a₂ : α) : (∃ a, a₁ < a ∧ a < a₂) ∨ (∀ a, a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁

Full source

theorem dense_or_discrete [LinearOrder α] (a₁ a₂ : α) :
    (∃ a, a₁ < a ∧ a < a₂) ∨ (∀ a, a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁ :=
  or_iff_not_imp_left.2 fun h ↦
    ⟨fun a ha₁ ↦ le_of_not_gt fun ha₂ ↦ h ⟨a, ha₁, ha₂⟩,
     fun a ha₂ ↦ le_of_not_gt fun ha₁ ↦ h ⟨a, ha₁, ha₂⟩⟩

Dichotomy of Dense or Discrete in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered set, and let $a_1, a_2 \in \alpha$. Then either there exists an element $a \in \alpha$ such that $a_1 < a < a_2$, or both of the following hold: 1. For every $a \in \alpha$, if $a_1 < a$ then $a_2 \leq a$. 2. For every $a \in \alpha$, if $a < a_2$ then $a \leq a_1$.

PUnit.instLinearOrder instance

: LinearOrder PUnit

Full source

instance instLinearOrder : LinearOrder PUnit where
  le  := fun _ _ ↦ True
  lt  := fun _ _ ↦ False
  max := fun _ _ ↦ unit
  min := fun _ _ ↦ unit
  toDecidableEq := inferInstance
  toDecidableLE := fun _ _ ↦ Decidable.isTrue trivial
  toDecidableLT := fun _ _ ↦ Decidable.isFalse id
  le_refl     := by intros; trivial
  le_trans    := by intros; trivial
  le_total    := by intros; exact Or.inl trivial
  le_antisymm := by intros; rfl
  lt_iff_le_not_le := by simp only [not_true, and_false, forall_const]

Linear Order on the Unit Type

Informal description

The unit type `PUnit` is equipped with a canonical linear order where all elements are considered equal.

PUnit.max_eq theorem

: max a b = unit

Full source

theorem max_eq : max a b = unit :=
  rfl

Maximum in Unit Type is Unique Element

Informal description

For any elements $a$ and $b$ of the unit type, the maximum of $a$ and $b$ is equal to the unique element of the unit type.

PUnit.min_eq theorem

: min a b = unit

Full source

theorem min_eq : min a b = unit :=
  rfl

Minimum in Unit Type is Unique Element

Informal description

For any elements $a$ and $b$ of the unit type, the minimum of $a$ and $b$ is equal to the unique element of the unit type.

PUnit.le theorem

: a ≤ b

Full source

protected theorem le : a ≤ b :=
  trivial

All Elements are Comparable in the Unit Type

Informal description

For any two elements $a$ and $b$ of the unit type `PUnit`, the relation $a \leq b$ holds.

PUnit.not_lt theorem

: ¬a < b

Full source

theorem not_lt : ¬a < b :=
  not_false

No Strict Order on the Unit Type

Informal description

For any elements $a$ and $b$ of the unit type `PUnit`, the relation $a < b$ does not hold.

PUnit.instDenselyOrdered instance

: DenselyOrdered PUnit

Full source

instance : DenselyOrdered PUnit :=
  ⟨fun _ _ ↦ False.elim⟩

Dense Order on the Unit Type

Informal description

The unit type `PUnit` is densely ordered.

Prop.le instance

: LE Prop

Full source

/-- Propositions form a complete boolean algebra, where the `≤` relation is given by implication. -/
instance Prop.le : LE Prop :=
  ⟨(· → ·)⟩

Implication as an Order on Propositions

Informal description

The set of propositions forms a partially ordered set where the order relation $\leq$ is given by implication. That is, for any two propositions $P$ and $Q$, we have $P \leq Q$ if and only if $P$ implies $Q$.

le_Prop_eq theorem

: ((· ≤ ·) : Prop → Prop → Prop) = (· → ·)

Full source

@[simp]
theorem le_Prop_eq : ((· ≤ ·) : Prop → Prop → Prop) = (· → ·) :=
  rfl

Equivalence of Propositional Order and Implication

Informal description

The order relation $\leq$ on propositions is equal to the implication relation $\to$, i.e., for any two propositions $P$ and $Q$, we have $P \leq Q$ if and only if $P \to Q$.

subrelation_iff_le theorem

{r s : α → α → Prop} : Subrelation r s ↔ r ≤ s

Full source

theorem subrelation_iff_le {r s : α → α → Prop} : SubrelationSubrelation r s ↔ r ≤ s :=
  Iff.rfl

Subrelation Equivalence to Implication Order

Informal description

For any two binary relations $r$ and $s$ on a type $\alpha$, the subrelation property $r \subseteq s$ holds if and only if $r$ is pointwise less than or equal to $s$ in the implication order on relations.

Prop.partialOrder instance

: PartialOrder Prop

Full source

instance Prop.partialOrder : PartialOrder Prop where
  __ := Prop.le
  le_refl _ := id
  le_trans _ _ _ f g := g ∘ f
  le_antisymm _ _ Hab Hba := propext ⟨Hab, Hba⟩

Implication Order on Propositions

Informal description

The set of propositions forms a partial order where the order relation $\leq$ is given by implication. That is, for any two propositions $P$ and $Q$, we have $P \leq Q$ if and only if $P$ implies $Q$.

AsLinearOrder definition

(α : Type*)

Full source

/-- Type synonym to create an instance of `LinearOrder` from a `PartialOrder` and `IsTotal α (≤)` -/
def AsLinearOrder (α : Type*)  :=
  α

Linear order promotion from a total partial order

Informal description

The type synonym `AsLinearOrder α` promotes a partial order on `α` to a linear order, given that the relation `≤` is total on `α`.

instInhabitedAsLinearOrder instance

[Inhabited α] : Inhabited (AsLinearOrder α)

Full source

instance [Inhabited α] : Inhabited (AsLinearOrder α) :=
  ⟨(default : α)⟩

Inhabitedness of Linear Order Promotion

Informal description

For any inhabited type $\alpha$, the type synonym $\text{AsLinearOrder}\ \alpha$ is also inhabited.

AsLinearOrder.linearOrder instance

[PartialOrder α] [IsTotal α (· ≤ ·)] : LinearOrder (AsLinearOrder α)

Full source

noncomputable instance AsLinearOrder.linearOrder [PartialOrder α] [IsTotal α (· ≤ ·)] :
    LinearOrder (AsLinearOrder α) where
  __ := inferInstanceAs (PartialOrder α)
  le_total := @total_of α (· ≤ ·) _
  toDecidableLE := Classical.decRel _

Linear Order Structure on AsLinearOrder

Informal description

For any type $\alpha$ with a partial order and a total order relation $\leq$, the type synonym $\text{AsLinearOrder}\ \alpha$ can be equipped with a linear order structure.

Mathlib.Order.Basic

Type synonyms

Transferring orders

Extra class

Notes

TODO

Tags