Mathlib.Order.RelClasses

IsRefl.swap theorem

(r) [IsRefl α r] : IsRefl α (swap r)

Full source

theorem IsRefl.swap (r) [IsRefl α r] : IsRefl α (swap r) :=
  ⟨refl_of r⟩

Reflexivity is Preserved Under Relation Swapping

Informal description

For any reflexive relation $r$ on a type $\alpha$, the swapped relation $\operatorname{swap}\, r$ is also reflexive. That is, if $r$ satisfies $r\, x\, x$ for all $x \in \alpha$, then $\operatorname{swap}\, r$ satisfies $\operatorname{swap}\, r\, x\, x$ for all $x \in \alpha$.

IsIrrefl.swap theorem

(r) [IsIrrefl α r] : IsIrrefl α (swap r)

Full source

theorem IsIrrefl.swap (r) [IsIrrefl α r] : IsIrrefl α (swap r) :=
  ⟨irrefl_of r⟩

Irreflexivity is preserved under relation swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is irreflexive (i.e., $\forall x \in \alpha, \neg r(x, x)$), then the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is also irreflexive.

IsTrans.swap theorem

(r) [IsTrans α r] : IsTrans α (swap r)

Full source

theorem IsTrans.swap (r) [IsTrans α r] : IsTrans α (swap r) :=
  ⟨fun _ _ _ h₁ h₂ => trans_of r h₂ h₁⟩

Transitivity is Preserved Under Relation Swapping

Informal description

For any transitive relation $r$ on a type $\alpha$, the swapped relation $\operatorname{swap}\, r$ is also transitive. That is, if $r$ satisfies $\forall x\, y\, z \in \alpha, r\, x\, y \land r\, y\, z \to r\, x\, z$, then $\operatorname{swap}\, r$ satisfies $\forall x\, y\, z \in \alpha, \operatorname{swap}\, r\, x\, y \land \operatorname{swap}\, r\, y\, z \to \operatorname{swap}\, r\, x\, z$.

IsAntisymm.swap theorem

(r) [IsAntisymm α r] : IsAntisymm α (swap r)

Full source

theorem IsAntisymm.swap (r) [IsAntisymm α r] : IsAntisymm α (swap r) :=
  ⟨fun _ _ h₁ h₂ => _root_.antisymm h₂ h₁⟩

Antisymmetry is preserved under relation swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is antisymmetric (i.e., $\forall x y \in \alpha, r(x, y) \land r(y, x) \to x = y$), then the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is also antisymmetric.

IsAsymm.swap theorem

(r) [IsAsymm α r] : IsAsymm α (swap r)

Full source

theorem IsAsymm.swap (r) [IsAsymm α r] : IsAsymm α (swap r) :=
  ⟨fun _ _ h₁ h₂ => asymm_of r h₂ h₁⟩

Asymmetry is preserved under relation swapping

Informal description

For any relation $r$ on a type $\alpha$, if $r$ is asymmetric (i.e., $r\,x\,y$ implies $\neg r\,y\,x$ for all $x, y \in \alpha$), then the swapped relation $\operatorname{swap}\,r$ (defined by $\operatorname{swap}\,r\,y\,x = r\,x\,y$) is also asymmetric.

IsTotal.swap theorem

(r) [IsTotal α r] : IsTotal α (swap r)

Full source

theorem IsTotal.swap (r) [IsTotal α r] : IsTotal α (swap r) :=
  ⟨fun a b => (total_of r a b).symm⟩

Total Relation Property Preserved Under Argument Swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is total (i.e., for any $x, y \in \alpha$, either $r\,x\,y$ or $r\,y\,x$ holds), then the swapped relation $\operatorname{swap}\,r$ (defined by $(\operatorname{swap}\,r)\,y\,x = r\,x\,y$) is also total.

IsTrichotomous.swap theorem

(r) [IsTrichotomous α r] : IsTrichotomous α (swap r)

Full source

theorem IsTrichotomous.swap (r) [IsTrichotomous α r] : IsTrichotomous α (swap r) :=
  ⟨fun a b => by simpa [Function.swap, or_comm, or_left_comm] using trichotomous_of r a b⟩

Trichotomy Property Preserved Under Relation Swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is trichotomous (i.e., for any $x, y \in \alpha$, exactly one of $x \mathbin{r} y$, $x = y$, or $y \mathbin{r} x$ holds), then the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)\, y\, x = r\, x\, y$) is also trichotomous.

IsPreorder.swap theorem

(r) [IsPreorder α r] : IsPreorder α (swap r)

Full source

theorem IsPreorder.swap (r) [IsPreorder α r] : IsPreorder α (swap r) :=
  { @IsRefl.swap α r _, @IsTrans.swap α r _ with }

Preorder Properties Preserved Under Relation Swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is a preorder (i.e., reflexive and transitive), then the swapped relation $\operatorname{swap}\,r$ (defined by $(\operatorname{swap}\,r)\,y\,x = r\,x\,y$) is also a preorder.

IsStrictOrder.swap theorem

(r) [IsStrictOrder α r] : IsStrictOrder α (swap r)

Full source

theorem IsStrictOrder.swap (r) [IsStrictOrder α r] : IsStrictOrder α (swap r) :=
  { @IsIrrefl.swap α r _, @IsTrans.swap α r _ with }

Strict Order Property Preserved Under Relation Swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is a strict order (i.e., it is irreflexive and transitive), then the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is also a strict order.

IsPartialOrder.swap theorem

(r) [IsPartialOrder α r] : IsPartialOrder α (swap r)

Full source

theorem IsPartialOrder.swap (r) [IsPartialOrder α r] : IsPartialOrder α (swap r) :=
  { @IsPreorder.swap α r _, @IsAntisymm.swap α r _ with }

Partial Order Properties Preserved Under Relation Swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is a partial order (i.e., reflexive, antisymmetric, and transitive), then the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is also a partial order.

partialOrderOfSO abbrev

(r) [IsStrictOrder α r] : PartialOrder α

Full source

/-- Construct a partial order from an `isStrictOrder` relation.

See note [reducible non-instances]. -/
abbrev partialOrderOfSO (r) [IsStrictOrder α r] : PartialOrder α where
  le x y := x = y ∨ r x y
  lt := r
  le_refl _ := Or.inl rfl
  le_trans x y z h₁ h₂ :=
    match y, z, h₁, h₂ with
    | _, _, Or.inl rfl, h₂ => h₂
    | _, _, h₁, Or.inl rfl => h₁
    | _, _, Or.inr h₁, Or.inr h₂ => Or.inr (_root_.trans h₁ h₂)
  le_antisymm x y h₁ h₂ :=
    match y, h₁, h₂ with
    | _, Or.inl rfl, _ => rfl
    | _, _, Or.inl rfl => rfl
    | _, Or.inr h₁, Or.inr h₂ => (asymm h₁ h₂).elim
  lt_iff_le_not_le x y :=
    ⟨fun h => ⟨Or.inr h, not_or_intro (fun e => by rw [e] at h; exact irrefl _ h) (asymm h)⟩,
      fun ⟨h₁, h₂⟩ => h₁.resolve_left fun e => h₂ <| e ▸ Or.inl rfl⟩

Partial Order Construction from Strict Order Relation

Informal description

Given a type $\alpha$ and a strict order relation $r$ on $\alpha$ (i.e., $r$ is irreflexive and transitive), the function `partialOrderOfSO` constructs a partial order structure on $\alpha$ from $r$.

linearOrderOfSTO abbrev

(r) [IsStrictTotalOrder α r] [DecidableRel r] : LinearOrder α

Full source

/-- Construct a linear order from an `IsStrictTotalOrder` relation.

See note [reducible non-instances]. -/
abbrev linearOrderOfSTO (r) [IsStrictTotalOrder α r] [DecidableRel r] : LinearOrder α :=
  let hD : DecidableRel (fun x y => x = y ∨ r x y) := fun x y => decidable_of_iff (¬r y x)
    ⟨fun h => ((trichotomous_of r y x).resolve_left h).imp Eq.symm id, fun h =>
      h.elim (fun h => h ▸ irrefl_of _ _) (asymm_of r)⟩
  { __ := partialOrderOfSO r
    le_total := fun x y =>
      match y, trichotomous_of r x y with
      | _, Or.inl h => Or.inl (Or.inr h)
      | _, Or.inr (Or.inl rfl) => Or.inl (Or.inl rfl)
      | _, Or.inr (Or.inr h) => Or.inr (Or.inr h),
    toMin := minOfLe,
    toMax := maxOfLe,
    toDecidableLE := hD }

Linear Order Construction from Strict Total Order Relation

Informal description

Given a type $\alpha$ and a strict total order relation $r$ on $\alpha$ (i.e., $r$ is irreflexive, transitive, and total), along with a decidable instance for $r$, the function `linearOrderOfSTO` constructs a linear order structure on $\alpha$ from $r$.

IsStrictTotalOrder.swap theorem

(r) [IsStrictTotalOrder α r] : IsStrictTotalOrder α (swap r)

Full source

theorem IsStrictTotalOrder.swap (r) [IsStrictTotalOrder α r] : IsStrictTotalOrder α (swap r) :=
  { IsTrichotomous.swap r, IsStrictOrder.swap r with }

Strict Total Order Property Preserved Under Relation Swapping

Informal description

For any binary relation $r$ on a type $\alpha$, if $r$ is a strict total order (i.e., it is irreflexive, transitive, and trichotomous), then the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is also a strict total order.

IsOrderConnected structure

(α : Type u) (lt : α → α → Prop)

Full source

/-- A connected order is one satisfying the condition `a < c → a < b ∨ b < c`.
  This is recognizable as an intuitionistic substitute for `a ≤ b ∨ b ≤ a` on
  the constructive reals, and is also known as negative transitivity,
  since the contrapositive asserts transitivity of the relation `¬ a < b`. -/
class IsOrderConnected (α : Type u) (lt : α → α → Prop) : Prop where
  /-- A connected order is one satisfying the condition `a < c → a < b ∨ b < c`. -/
  conn : ∀ a b c, lt a c → lt a b ∨ lt b c

Order connected relation

Informal description

A relation `lt` on a type `α` is called *order connected* if it satisfies the condition that for any elements `a`, `b`, `c` in `α`, if `a < c` then either `a < b` or `b < c`. This property is an intuitionistic substitute for the linear order condition `a ≤ b ∨ b ≤ a` and is also known as *negative transitivity*, since its contrapositive implies transitivity of the negation of the relation `¬ (a < b)`.

IsOrderConnected.neg_trans theorem

{r : α → α → Prop} [IsOrderConnected α r] {a b c} (h₁ : ¬r a b) (h₂ : ¬r b c) : ¬r a c

Full source

theorem IsOrderConnected.neg_trans {r : α → α → Prop} [IsOrderConnected α r] {a b c}
    (h₁ : ¬r a b) (h₂ : ¬r b c) : ¬r a c :=
  mt (IsOrderConnected.conn a b c) <| by simp [h₁, h₂]

Negative Transitivity of Order Connected Relations

Informal description

Let $\alpha$ be a type with an order connected relation $r$. For any elements $a, b, c \in \alpha$, if $\neg (a \mathbin{r} b)$ and $\neg (b \mathbin{r} c)$, then $\neg (a \mathbin{r} c)$.

isStrictWeakOrder_of_isOrderConnected theorem

[IsAsymm α r] [IsOrderConnected α r] : IsStrictWeakOrder α r

Full source

theorem isStrictWeakOrder_of_isOrderConnected [IsAsymm α r] [IsOrderConnected α r] :
    IsStrictWeakOrder α r :=
  { @IsAsymm.isIrrefl α r _ with
    trans := fun _ _ c h₁ h₂ => (IsOrderConnected.conn _ c _ h₁).resolve_right (asymm h₂),
    incomp_trans := fun _ _ _ ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ =>
      ⟨IsOrderConnected.neg_trans h₁ h₃, IsOrderConnected.neg_trans h₄ h₂⟩ }

Order Connected and Asymmetric Relations are Strict Weak Orders

Informal description

Let $\alpha$ be a type with an asymmetric and order connected relation $r$. Then $r$ is a strict weak order on $\alpha$.

isStrictOrderConnected_of_isStrictTotalOrder instance

[IsStrictTotalOrder α r] : IsOrderConnected α r

Full source

instance (priority := 100) isStrictOrderConnected_of_isStrictTotalOrder [IsStrictTotalOrder α r] :
    IsOrderConnected α r :=
  ⟨fun _ _ _ h ↦ (trichotomous _ _).imp_right
    fun o ↦ o.elim (fun e ↦ e ▸ h) fun h' ↦ _root_.trans h' h⟩

Strict Total Orders are Order Connected

Informal description

For any type $\alpha$ with a strict total order $r$, the relation $r$ is order connected.

InvImage.isTrichotomous theorem

[IsTrichotomous α r] {f : β → α} (h : Function.Injective f) : IsTrichotomous β (InvImage r f)

Full source

theorem InvImage.isTrichotomous [IsTrichotomous α r] {f : β → α} (h : Function.Injective f) :
    IsTrichotomous β (InvImage r f)  where
  trichotomous a b := trichotomous (f a) (f b) |>.imp3 id (h ·) id

Inverse Image Preserves Trichotomy of Relations

Informal description

Let $\alpha$ be a type with a trichotomous relation $r$ (i.e., for any $x, y \in \alpha$, exactly one of $x \mathrel{r} y$, $x = y$, or $y \mathrel{r} x$ holds). Given an injective function $f : \beta \to \alpha$, the relation on $\beta$ defined by $x \mathrel{r'} y \leftrightarrow f(x) \mathrel{r} f(y)$ is also trichotomous.

InvImage.isAsymm instance

[IsAsymm α r] (f : β → α) : IsAsymm β (InvImage r f)

Full source

instance InvImage.isAsymm [IsAsymm α r] (f : β → α) : IsAsymm β (InvImage r f) where
  asymm a b h h2 := IsAsymm.asymm (f a) (f b) h h2

Inverse Image Preserves Asymmetry of Relations

Informal description

For any type $\alpha$ with an asymmetric relation $r$ and any injective function $f : \beta \to \alpha$, the relation on $\beta$ defined by $x \mathrel{r'} y \leftrightarrow f(x) \mathrel{r} f(y)$ is also asymmetric.

IsWellFounded structure

(α : Type u) (r : α → α → Prop)

Full source

/-- A well-founded relation. Not to be confused with `IsWellOrder`. -/
@[mk_iff] class IsWellFounded (α : Type u) (r : α → α → Prop) : Prop where
  /-- The relation is `WellFounded`, as a proposition. -/
  wf : WellFounded r

Well-founded relation

Informal description

A structure representing a well-founded relation on a type `α`, where a relation `r : α → α → Prop` is well-founded if every non-empty subset of `α` has a minimal element with respect to `r`. This is distinct from `IsWellOrder`, which additionally requires the relation to be total and transitive.

WellFoundedRelation.isWellFounded instance

[h : WellFoundedRelation α] : IsWellFounded α WellFoundedRelation.rel

Full source

instance WellFoundedRelation.isWellFounded [h : WellFoundedRelation α] :
    IsWellFounded α WellFoundedRelation.rel :=
  { h with }

Well-founded Relations are Well-Founded

Informal description

For any type $\alpha$ with a well-founded relation, the relation is well-founded.

WellFoundedRelation.asymmetric theorem

{α : Sort*} [WellFoundedRelation α] {a b : α} : WellFoundedRelation.rel a b → ¬WellFoundedRelation.rel b a

Full source

theorem WellFoundedRelation.asymmetric {α : Sort*} [WellFoundedRelation α] {a b : α} :
    WellFoundedRelation.rel a b → ¬ WellFoundedRelation.rel b a :=
  fun hab hba => WellFoundedRelation.asymmetric hba hab
termination_by a

Asymmetry of Well-Founded Relations

Informal description

For any type $\alpha$ with a well-founded relation $\mathrm{rel}$, if $\mathrm{rel}(a, b)$ holds for elements $a, b \in \alpha$, then $\mathrm{rel}(b, a)$ does not hold.

WellFoundedRelation.asymmetric₃ theorem

 {α : Sort*} [WellFoundedRelation α] {a b c : α} :
  WellFoundedRelation.rel a b → WellFoundedRelation.rel b c → ¬WellFoundedRelation.rel c a

Full source

theorem WellFoundedRelation.asymmetric₃ {α : Sort*} [WellFoundedRelation α] {a b c : α} :
    WellFoundedRelation.rel a b → WellFoundedRelation.rel b c → ¬ WellFoundedRelation.rel c a :=
  fun hab hbc hca => WellFoundedRelation.asymmetric₃ hca hab hbc
termination_by a

Asymmetry of Well-Founded Relation Triples

Informal description

Let $\alpha$ be a type with a well-founded relation $\mathrm{rel}$. For any elements $a, b, c \in \alpha$, if $\mathrm{rel}(a, b)$ and $\mathrm{rel}(b, c)$ hold, then $\mathrm{rel}(c, a)$ does not hold.

WellFounded.prod_lex theorem

 {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Prod.Lex ra rb)

Full source

lemma WellFounded.prod_lex {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra)
    (hb : WellFounded rb) : WellFounded (Prod.Lex ra rb) :=
  (Prod.lex ⟨_, ha⟩ ⟨_, hb⟩).wf

Well-Foundedness of Lexicographic Product Relation

Informal description

Let $\alpha$ and $\beta$ be types with relations $r_a : \alpha \to \alpha \to \mathrm{Prop}$ and $r_b : \beta \to \beta \to \mathrm{Prop}$ respectively. If $r_a$ is well-founded on $\alpha$ and $r_b$ is well-founded on $\beta$, then the lexicographic product relation $\mathrm{Prod.Lex}\,r_a\,r_b$ is well-founded on $\alpha \times \beta$.

WellFounded.psigma_lex theorem

 {α : Sort*} {β : α → Sort*} {r : α → α → Prop} {s : ∀ a : α, β a → β a → Prop} (ha : WellFounded r)
  (hb : ∀ x, WellFounded (s x)) : WellFounded (Lex r s)

Full source

/-- The lexicographical order of well-founded relations is well-founded. -/
theorem WellFounded.psigma_lex
    {α : Sort*} {β : α → Sort*} {r : α → α → Prop} {s : ∀ a : α, β a → β a → Prop}
    (ha : WellFounded r) (hb : ∀ x, WellFounded (s x)) : WellFounded (Lex r s) :=
  WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) hb b

Well-Foundedness of Lexicographic Order on Dependent Sum Types

Informal description

Let $\alpha$ be a type and $\beta : \alpha \to \text{Sort}^*$ be a family of types indexed by $\alpha$. Given a well-founded relation $r$ on $\alpha$ and for each $x \in \alpha$, a well-founded relation $s_x$ on $\beta(x)$, the lexicographical order on the dependent sum type $\Sigma_{a:\alpha} \beta(a)$ is well-founded.

WellFounded.psigma_revLex theorem

 {α : Sort*} {β : Sort*} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :
  WellFounded (RevLex r s)

Full source

theorem WellFounded.psigma_revLex
    {α : Sort*} {β : Sort*} {r : α → α → Prop} {s : β → β → Prop}
    (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
  WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a

Well-foundedness of Reverse Lexicographic Order on Product Types

Informal description

Let $\alpha$ and $\beta$ be types, and let $r : \alpha \to \alpha \to \mathrm{Prop}$ and $s : \beta \to \beta \to \mathrm{Prop}$ be binary relations on $\alpha$ and $\beta$ respectively. If $r$ is well-founded on $\alpha$ and $s$ is well-founded on $\beta$, then the reverse lexicographic order on the product type $\alpha \times \beta$ is also well-founded.

WellFounded.psigma_skipLeft theorem

(α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFounded s) : WellFounded (SkipLeft α s)

Full source

theorem WellFounded.psigma_skipLeft (α : Type u) {β : Type v} {s : β → β → Prop}
    (hb : WellFounded s) : WellFounded (SkipLeft α s) :=
  psigma_revLex emptyWf.wf hb

Well-foundedness of SkipLeft Relation on Product Types

Informal description

Let $\alpha$ be a type and $\beta$ be another type with a well-founded relation $s : \beta \to \beta \to \mathrm{Prop}$. Then the relation $\mathrm{SkipLeft} \, \alpha \, s$ on $\alpha \times \beta$ is well-founded, where $\mathrm{SkipLeft}$ ignores the first component and compares the second component using $s$.

IsWellFounded.induction theorem

{C : α → Prop} (a : α) (ind : ∀ x, (∀ y, r y x → C y) → C x) : C a

Full source

/-- Induction on a well-founded relation. -/
theorem induction {C : α → Prop} (a : α) (ind : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
  wf.induction _ ind

Well-founded Induction Principle

Informal description

Let $\alpha$ be a type equipped with a well-founded relation $r$. For any predicate $C : \alpha \to \mathrm{Prop}$ and any element $a \in \alpha$, if for every $x \in \alpha$ the implication $(\forall y \in \alpha, r(y,x) \to C(y)) \to C(x)$ holds, then $C(a)$ holds.

IsWellFounded.apply theorem

: ∀ a, Acc r a

Full source

/-- All values are accessible under the well-founded relation. -/
theorem apply : ∀ a, Acc r a :=
  wf.apply

Accessibility of all elements under a well-founded relation

Informal description

For every element $a$ in a type $\alpha$ with a well-founded relation $r$, $a$ is accessible under $r$, meaning there is no infinite decreasing sequence starting from $a$.

IsWellFounded.fix definition

{C : α → Sort*} : (∀ x : α, (∀ y : α, r y x → C y) → C x) → ∀ x : α, C x

Full source

/-- Creates data, given a way to generate a value from all that compare as less under a well-founded
relation. See also `IsWellFounded.fix_eq`. -/
def fix {C : α → Sort*} : (∀ x : α, (∀ y : α, r y x → C y) → C x) → ∀ x : α, C x :=
  wf.fix

Well-founded recursion

Informal description

Given a well-founded relation `r` on a type `α` and a dependent type `C : α → Sort*`, the function `IsWellFounded.fix` takes as input a function `F` that for any `x : α` produces an element of `C x` using values from all `y` such that `r y x`, and returns a function that for any `x : α` produces an element of `C x` by recursively applying `F`. This satisfies the fixpoint property `fix r F x = F x (λ y _, fix r F y)`.

IsWellFounded.fix_eq theorem

{C : α → Sort*} (F : ∀ x : α, (∀ y : α, r y x → C y) → C x) : ∀ x, fix r F x = F x fun y _ => fix r F y

Full source

/-- The value from `IsWellFounded.fix` is built from the previous ones as specified. -/
theorem fix_eq {C : α → Sort*} (F : ∀ x : α, (∀ y : α, r y x → C y) → C x) :
    ∀ x, fix r F x = F x fun y _ => fix r F y :=
  wf.fix_eq F

Fixed Point Property of Well-Founded Recursion

Informal description

For any type $\alpha$ with a well-founded relation $r$, and for any dependent type $C : \alpha \to \text{Sort}*$, given a function $F$ that constructs an element of $C(x)$ for each $x \in \alpha$ using elements of $C(y)$ for all $y$ such that $r(y, x)$, the fixed point $\text{fix}_r F$ satisfies the equation: \[ \text{fix}_r F(x) = F(x, \lambda y \_, \text{fix}_r F(y)) \] for all $x \in \alpha$.

IsWellFounded.toWellFoundedRelation definition

: WellFoundedRelation α

Full source

/-- Derive a `WellFoundedRelation` instance from an `isWellFounded` instance. -/
def toWellFoundedRelation : WellFoundedRelation α :=
  ⟨r, IsWellFounded.wf⟩

Well-founded relation instance from `IsWellFounded`

Informal description

Given a well-founded relation `r` on a type `α`, this definition constructs a `WellFoundedRelation` instance for `α` by packaging `r` together with the proof that it is well-founded.

WellFounded.asymmetric theorem

{α : Sort*} {r : α → α → Prop} (h : WellFounded r) (a b) : r a b → ¬r b a

Full source

theorem WellFounded.asymmetric {α : Sort*} {r : α → α → Prop} (h : WellFounded r) (a b) :
    r a b → ¬r b a :=
  @WellFoundedRelation.asymmetric _ ⟨_, h⟩ _ _

Asymmetry of Well-Founded Relations

Informal description

For any type $\alpha$ and a well-founded relation $r$ on $\alpha$, if $r(a, b)$ holds for elements $a, b \in \alpha$, then $r(b, a)$ does not hold.

WellFounded.asymmetric₃ theorem

{α : Sort*} {r : α → α → Prop} (h : WellFounded r) (a b c) : r a b → r b c → ¬r c a

Full source

theorem WellFounded.asymmetric₃ {α : Sort*} {r : α → α → Prop} (h : WellFounded r) (a b c) :
    r a b → r b c → ¬r c a :=
  @WellFoundedRelation.asymmetric₃ _ ⟨_, h⟩ _ _ _

Triple Asymmetry Property of Well-Founded Relations

Informal description

Let $\alpha$ be a type and $r$ be a well-founded relation on $\alpha$. For any elements $a, b, c \in \alpha$, if $r(a, b)$ and $r(b, c)$ hold, then $r(c, a)$ does not hold.

instIsAsymmOfIsWellFounded instance

(r : α → α → Prop) [IsWellFounded α r] : IsAsymm α r

Full source

instance (priority := 100) (r : α → α → Prop) [IsWellFounded α r] : IsAsymm α r :=
  ⟨IsWellFounded.wf.asymmetric⟩

Asymmetry of Well-Founded Relations

Informal description

For any type $\alpha$ and a well-founded relation $r$ on $\alpha$, the relation $r$ is asymmetric. That is, for any elements $a, b \in \alpha$, if $r(a, b)$ holds, then $r(b, a)$ does not hold.

instIsIrreflOfIsWellFounded instance

(r : α → α → Prop) [IsWellFounded α r] : IsIrrefl α r

Full source

instance (priority := 100) (r : α → α → Prop) [IsWellFounded α r] : IsIrrefl α r :=
  IsAsymm.isIrrefl

Irreflexivity of Well-Founded Relations

Informal description

For any type $\alpha$ and a well-founded relation $r$ on $\alpha$, the relation $r$ is irreflexive. That is, for any element $a \in \alpha$, $r(a, a)$ does not hold.

instIsWellFoundedTransGen instance

(r : α → α → Prop) [i : IsWellFounded α r] : IsWellFounded α (Relation.TransGen r)

Full source

instance (r : α → α → Prop) [i : IsWellFounded α r] : IsWellFounded α (Relation.TransGen r) :=
  ⟨i.wf.transGen⟩

Well-foundedness of the Transitive Closure

Informal description

For any type $\alpha$ with a well-founded relation $r$, the transitive closure of $r$ is also well-founded.

WellFoundedLT abbrev

(α : Type*) [LT α] : Prop

Full source

/-- A class for a well founded relation `<`. -/
abbrev WellFoundedLT (α : Type*) [LT α] : Prop :=
  IsWellFounded α (· < ·)

Well-founded strict less-than relation

Informal description

A type `α` with a strict less-than relation `<` is said to satisfy `WellFoundedLT` if the relation `<` is well-founded, meaning every non-empty subset of `α` has a minimal element with respect to `<`.

WellFoundedGT abbrev

(α : Type*) [LT α] : Prop

Full source

/-- A class for a well founded relation `>`. -/
abbrev WellFoundedGT (α : Type*) [LT α] : Prop :=
  IsWellFounded α (· > ·)

Well-foundedness of the "greater than" relation

Informal description

A type `α` equipped with a "greater than" relation `>` is said to satisfy `WellFoundedGT` if the relation `>` is well-founded on `α`, meaning every non-empty subset of `α` has a minimal element with respect to `>`.

wellFounded_lt theorem

[LT α] [WellFoundedLT α] : @WellFounded α (· < ·)

Full source

lemma wellFounded_lt [LT α] [WellFoundedLT α] : @WellFounded α (· < ·) := IsWellFounded.wf

Well-foundedness of the Less Than Relation

Informal description

For any type $\alpha$ with a strict less-than relation $<$ that is well-founded, the relation $<$ is well-founded on $\alpha$.

wellFounded_gt theorem

[LT α] [WellFoundedGT α] : @WellFounded α (· > ·)

Full source

lemma wellFounded_gt [LT α] [WellFoundedGT α] : @WellFounded α (· > ·) := IsWellFounded.wf

Well-foundedness of the Greater Than Relation

Informal description

For any type $\alpha$ with a strict order relation $<$ such that the "greater than" relation $>$ is well-founded, the relation $>$ is well-founded on $\alpha$.

instWellFoundedGTOrderDualOfWellFoundedLT instance

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

Full source

instance (priority := 100) (α : Type*) [LT α] [h : WellFoundedLT α] : WellFoundedGT αᵒᵈ :=
  h

Well-foundedness of Greater Than in Order Dual from Less Than

Informal description

For any type $\alpha$ with a strict less-than relation $<$ that is well-founded, the order dual $\alpha^{\text{op}}$ (where $>$ is interpreted as $<$) has a well-founded "greater than" relation.

instWellFoundedLTOrderDualOfWellFoundedGT instance

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

Full source

instance (priority := 100) (α : Type*) [LT α] [h : WellFoundedGT α] : WellFoundedLT αᵒᵈ :=
  h

Well-foundedness of Less Than in Order Dual from Greater Than

Informal description

For any type $\alpha$ with a "greater than" relation $>$ that is well-founded, the order dual $\alpha^{\text{op}}$ (where $<$ is interpreted as $>$) has a well-founded "less than" relation.

wellFoundedGT_dual_iff theorem

(α : Type*) [LT α] : WellFoundedGT αᵒᵈ ↔ WellFoundedLT α

Full source

theorem wellFoundedGT_dual_iff (α : Type*) [LT α] : WellFoundedGTWellFoundedGT αᵒᵈ ↔ WellFoundedLT α :=
  ⟨fun h => ⟨h.wf⟩, fun h => ⟨h.wf⟩⟩

Well-foundedness Duality: $\text{WellFoundedGT}(\alpha^{\text{op}}) \leftrightarrow \text{WellFoundedLT}(\alpha)$

Informal description

For any type $\alpha$ with a strict less-than relation $<$, the order dual $\alpha^{\text{op}}$ has a well-founded "greater than" relation if and only if $\alpha$ has a well-founded "less than" relation.

wellFoundedLT_dual_iff theorem

(α : Type*) [LT α] : WellFoundedLT αᵒᵈ ↔ WellFoundedGT α

Full source

theorem wellFoundedLT_dual_iff (α : Type*) [LT α] : WellFoundedLTWellFoundedLT αᵒᵈ ↔ WellFoundedGT α :=
  ⟨fun h => ⟨h.wf⟩, fun h => ⟨h.wf⟩⟩

Duality of Well-foundedness: $\text{WellFoundedLT}(\alpha^{\text{op}}) \leftrightarrow \text{WellFoundedGT}(\alpha)$

Informal description

For any type $\alpha$ with a strict less-than relation $<$, the order dual $\alpha^{\text{op}}$ has a well-founded "less than" relation if and only if $\alpha$ has a well-founded "greater than" relation.

IsWellOrder structure

(α : Type u) (r : α → α → Prop) : Prop
    extends IsTrichotomous α r, IsTrans α r, IsWellFounded α r

Full source

/-- A well order is a well-founded linear order. -/
class IsWellOrder (α : Type u) (r : α → α → Prop) : Prop
    extends IsTrichotomous α r, IsTrans α r, IsWellFounded α r

Well-order relation

Informal description

A relation $ r $ on a type $ \alpha $ is a well-order if it satisfies the following properties: 1. **Trichotomy**: For any two elements $ x, y \in \alpha $, exactly one of the following holds: $ r(x, y) $, $ x = y $, or $ r(y, x) $. 2. **Transitivity**: For any three elements $ x, y, z \in \alpha $, if $ r(x, y) $ and $ r(y, z) $ hold, then $ r(x, z) $ also holds. 3. **Well-foundedness**: Every non-empty subset of $ \alpha $ has a minimal element with respect to $ r $.

instIsStrictTotalOrderOfIsWellOrder instance

{α} (r : α → α → Prop) [IsWellOrder α r] : IsStrictTotalOrder α r

Full source

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] :
    IsStrictTotalOrder α r where

Well-Orders are Strict Total Orders

Informal description

For any type $\alpha$ and relation $r$ on $\alpha$, if $r$ is a well-order, then $r$ is a strict total order. That is, $r$ is irreflexive, transitive, and satisfies the trichotomy property.

instIsTrichotomousOfIsWellOrder instance

{α} (r : α → α → Prop) [IsWellOrder α r] : IsTrichotomous α r

Full source

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsTrichotomous α r := by
  infer_instance

Trichotomy Property of Well-Orders

Informal description

For any type $\alpha$ and relation $r$ on $\alpha$, if $r$ is a well-order, then $r$ satisfies the trichotomy property: for any two elements $x, y \in \alpha$, exactly one of $r(x, y)$, $x = y$, or $r(y, x)$ holds.

instIsTransOfIsWellOrder instance

{α} (r : α → α → Prop) [IsWellOrder α r] : IsTrans α r

Full source

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsTrans α r := by
  infer_instance

Transitivity of Well-Orders

Informal description

For any type $\alpha$ and relation $r$ on $\alpha$, if $r$ is a well-order, then $r$ is transitive. That is, for any three elements $x, y, z \in \alpha$, if $r(x, y)$ and $r(y, z)$ hold, then $r(x, z)$ also holds.

instIsIrreflOfIsWellOrder instance

{α} (r : α → α → Prop) [IsWellOrder α r] : IsIrrefl α r

Full source

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsIrrefl α r := by
  infer_instance

Irreflexivity of Well-Orders

Informal description

For any type $\alpha$ and relation $r$ on $\alpha$, if $r$ is a well-order, then $r$ is irreflexive. That is, for any element $x \in \alpha$, the relation $r(x, x)$ does not hold.

instIsAsymmOfIsWellOrder instance

{α} (r : α → α → Prop) [IsWellOrder α r] : IsAsymm α r

Full source

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsAsymm α r := by
  infer_instance

Asymmetry of Well-Order Relations

Informal description

For any type $\alpha$ and a well-order relation $r$ on $\alpha$, the relation $r$ is asymmetric. That is, for any elements $a, b \in \alpha$, if $r(a, b)$ holds, then $r(b, a)$ does not hold.

WellFoundedLT.induction theorem

{C : α → Prop} (a : α) (ind : ∀ x, (∀ y, y < x → C y) → C x) : C a

Full source

/-- Inducts on a well-founded `<` relation. -/
theorem induction {C : α → Prop} (a : α) (ind : ∀ x, (∀ y, y < x → C y) → C x) : C a :=
  IsWellFounded.induction _ _ ind

Well-founded Induction Principle for Strict Orders

Informal description

Let $\alpha$ be a type with a well-founded strict less-than relation $<$. For any predicate $C : \alpha \to \mathrm{Prop}$ and any element $a \in \alpha$, if for every $x \in \alpha$ the implication $(\forall y \in \alpha, y < x \to C(y)) \to C(x)$ holds, then $C(a)$ holds.

WellFoundedLT.apply theorem

: ∀ a : α, Acc (· < ·) a

Full source

/-- All values are accessible under the well-founded `<`. -/
theorem apply : ∀ a : α, Acc (· < ·) a :=
  IsWellFounded.apply _

Accessibility under Well-Founded Strict Order

Informal description

For every element $a$ in a type $\alpha$ with a well-founded strict less-than relation $<$, $a$ is accessible under $<$, meaning there is no infinite decreasing sequence starting from $a$.

WellFoundedLT.fix definition

{C : α → Sort*} : (∀ x : α, (∀ y : α, y < x → C y) → C x) → ∀ x : α, C x

Full source

/-- Creates data, given a way to generate a value from all that compare as lesser. See also
`WellFoundedLT.fix_eq`. -/
def fix {C : α → Sort*} : (∀ x : α, (∀ y : α, y < x → C y) → C x) → ∀ x : α, C x :=
  IsWellFounded.fix (· < ·)

Well-founded recursion for strict orders

Informal description

Given a type $\alpha$ with a well-founded strict less-than relation $<$ and a dependent type $C : \alpha \to \mathrm{Sort}*$, the function $\mathrm{WellFoundedLT.fix}$ takes as input a function $F$ that for any $x \in \alpha$ produces an element of $C x$ using values from all $y \in \alpha$ such that $y < x$, and returns a function that for any $x \in \alpha$ produces an element of $C x$ by recursively applying $F$. This satisfies the fixpoint property $\mathrm{fix}\, F\, x = F\, x\, (\lambda y\, \_, \mathrm{fix}\, F\, y)$.

WellFoundedLT.fix_eq theorem

{C : α → Sort*} (F : ∀ x : α, (∀ y : α, y < x → C y) → C x) : ∀ x, fix F x = F x fun y _ => fix F y

Full source

/-- The value from `WellFoundedLT.fix` is built from the previous ones as specified. -/
theorem fix_eq {C : α → Sort*} (F : ∀ x : α, (∀ y : α, y < x → C y) → C x) :
    ∀ x, fix F x = F x fun y _ => fix F y :=
  IsWellFounded.fix_eq _ F

Fixed-point equation for well-founded recursion on strict orders

Informal description

For any type $\alpha$ with a well-founded strict less-than relation $<$ and any dependent type $C : \alpha \to \mathrm{Sort}*$, given a function $F$ that constructs an element of $C(x)$ for each $x \in \alpha$ using elements of $C(y)$ for all $y < x$, the fixed point $\mathrm{fix}\, F$ satisfies the equation: \[ \mathrm{fix}\, F\, x = F\, x\, (\lambda y\, \_, \mathrm{fix}\, F\, y) \] for all $x \in \alpha$.

WellFoundedLT.toWellFoundedRelation definition

: WellFoundedRelation α

Full source

/-- Derive a `WellFoundedRelation` instance from a `WellFoundedLT` instance. -/
def toWellFoundedRelation : WellFoundedRelation α :=
  IsWellFounded.toWellFoundedRelation (· < ·)

Well-founded relation instance from well-founded less-than

Informal description

Given a type `α` with a well-founded strict less-than relation `<`, this definition constructs a `WellFoundedRelation` instance for `α` by packaging the relation `<` together with the proof that it is well-founded.

WellFoundedGT.induction theorem

{C : α → Prop} (a : α) (ind : ∀ x, (∀ y, x < y → C y) → C x) : C a

Full source

/-- Inducts on a well-founded `>` relation. -/
theorem induction {C : α → Prop} (a : α) (ind : ∀ x, (∀ y, x < y → C y) → C x) : C a :=
  IsWellFounded.induction _ _ ind

Well-founded Induction Principle for Greater-Than Relation

Informal description

Let $\alpha$ be a type with a well-founded "greater than" relation $>$. For any predicate $C : \alpha \to \mathrm{Prop}$ and any element $a \in \alpha$, if for every $x \in \alpha$ the implication $(\forall y \in \alpha, x < y \to C(y)) \to C(x)$ holds, then $C(a)$ holds.

WellFoundedGT.apply theorem

: ∀ a : α, Acc (· > ·) a

Full source

/-- All values are accessible under the well-founded `>`. -/
theorem apply : ∀ a : α, Acc (· > ·) a :=
  IsWellFounded.apply _

Accessibility under well-founded greater-than relation

Informal description

For every element $a$ in a type $\alpha$ with a well-founded "greater than" relation $>$, $a$ is accessible under $>$, meaning there is no infinite decreasing sequence starting from $a$.

WellFoundedGT.fix definition

{C : α → Sort*} : (∀ x : α, (∀ y : α, x < y → C y) → C x) → ∀ x : α, C x

Full source

/-- Creates data, given a way to generate a value from all that compare as greater. See also
`WellFoundedGT.fix_eq`. -/
def fix {C : α → Sort*} : (∀ x : α, (∀ y : α, x < y → C y) → C x) → ∀ x : α, C x :=
  IsWellFounded.fix (· > ·)

Well-founded recursion for greater-than relation

Informal description

Given a type $\alpha$ with a well-founded "greater than" relation $>$, and a dependent type $C : \alpha \to \text{Sort}*$, the function $\text{WellFoundedGT.fix}$ takes as input a function $F$ that for any $x : \alpha$ produces an element of $C x$ using values from all $y$ such that $x < y$, and returns a function that for any $x : \alpha$ produces an element of $C x$ by recursively applying $F$. This satisfies the fixpoint property $\text{fix } F x = F x (\lambda y \_, \text{fix } F y)$.

WellFoundedGT.fix_eq theorem

{C : α → Sort*} (F : ∀ x : α, (∀ y : α, x < y → C y) → C x) : ∀ x, fix F x = F x fun y _ => fix F y

Full source

/-- The value from `WellFoundedGT.fix` is built from the successive ones as specified. -/
theorem fix_eq {C : α → Sort*} (F : ∀ x : α, (∀ y : α, x < y → C y) → C x) :
    ∀ x, fix F x = F x fun y _ => fix F y :=
  IsWellFounded.fix_eq _ F

Fixed Point Property of Well-Founded Recursion for Greater-Than Relation

Informal description

For any type $\alpha$ with a well-founded "greater than" relation $>$, and for any dependent type $C : \alpha \to \text{Sort}*$, given a function $F$ that constructs an element of $C(x)$ for each $x \in \alpha$ using elements of $C(y)$ for all $y$ such that $x < y$, the fixed point $\text{fix } F$ satisfies the equation: \[ \text{fix } F(x) = F(x, \lambda y \_, \text{fix } F(y)) \] for all $x \in \alpha$.

WellFoundedGT.toWellFoundedRelation definition

: WellFoundedRelation α

Full source

/-- Derive a `WellFoundedRelation` instance from a `WellFoundedGT` instance. -/
def toWellFoundedRelation : WellFoundedRelation α :=
  IsWellFounded.toWellFoundedRelation (· > ·)

Well-founded relation instance from well-founded greater-than relation

Informal description

Given a type $\alpha$ with a well-founded "greater than" relation $>$, this definition constructs a `WellFoundedRelation` instance for $\alpha$ where the relation is $>$ and the well-foundedness proof is derived from the `WellFoundedGT` instance.

IsWellOrder.linearOrder definition

(r : α → α → Prop) [IsWellOrder α r] : LinearOrder α

Full source

/-- Construct a decidable linear order from a well-founded linear order. -/
noncomputable def IsWellOrder.linearOrder (r : α → α → Prop) [IsWellOrder α r] : LinearOrder α :=
  linearOrderOfSTO r

Linear order from well-order relation

Informal description

Given a type $\alpha$ and a well-order relation $r$ on $\alpha$, the function constructs a linear order structure on $\alpha$ from $r$. This linear order is derived from the strict total order properties of $r$ (irreflexivity, transitivity, and trichotomy) along with its well-foundedness.

IsWellOrder.toHasWellFounded definition

[LT α] [hwo : IsWellOrder α (· < ·)] : WellFoundedRelation α

Full source

/-- Derive a `WellFoundedRelation` instance from an `IsWellOrder` instance. -/
def IsWellOrder.toHasWellFounded [LT α] [hwo : IsWellOrder α (· < ·)] : WellFoundedRelation α where
  rel := (· < ·)
  wf := hwo.wf

Well-founded relation from a well-order

Informal description

Given a type `α` with a strict order `<` that is a well-order (i.e., it is trichotomous, transitive, and well-founded), this definition constructs a `WellFoundedRelation` instance for `α` where the relation is `<` and the well-foundedness proof is derived from the well-order property.

Subsingleton.isWellOrder theorem

[Subsingleton α] (r : α → α → Prop) [hr : IsIrrefl α r] : IsWellOrder α r

Full source

theorem Subsingleton.isWellOrder [Subsingleton α] (r : α → α → Prop) [hr : IsIrrefl α r] :
    IsWellOrder α r :=
  { hr with
    trichotomous := fun a b => Or.inr <| Or.inl <| Subsingleton.elim a b,
    trans := fun a b _ h => (not_rel_of_subsingleton r a b h).elim,
    wf := ⟨fun a => ⟨_, fun y h => (not_rel_of_subsingleton r y a h).elim⟩⟩ }

Well-Ordering on Subsingleton Types with Irreflexive Relations

Informal description

For any subsingleton type $\alpha$ (i.e., a type with at most one element) and any irreflexive relation $r$ on $\alpha$, the relation $r$ is a well-order on $\alpha$.

instIsWellOrderEmptyRelationOfSubsingleton instance

[Subsingleton α] : IsWellOrder α EmptyRelation

Full source

instance [Subsingleton α] : IsWellOrder α EmptyRelation :=
  Subsingleton.isWellOrder _

Empty Relation is a Well-Order on Subsingleton Types

Informal description

For any subsingleton type $\alpha$ (a type with at most one element), the empty relation is a well-order on $\alpha$.

instIsWellOrderOfIsEmpty instance

[IsEmpty α] (r : α → α → Prop) : IsWellOrder α r

Full source

instance (priority := 100) [IsEmpty α] (r : α → α → Prop) : IsWellOrder α r where
  trichotomous := isEmptyElim
  trans := isEmptyElim
  wf := wellFounded_of_isEmpty r

Empty Types Have Well-Ordered Relations

Informal description

For any empty type $\alpha$ and any binary relation $r$ on $\alpha$, the relation $r$ is a well-order on $\alpha$.

Prod.Lex.instIsWellFounded instance

[IsWellFounded α r] [IsWellFounded β s] : IsWellFounded (α × β) (Prod.Lex r s)

Full source

instance Prod.Lex.instIsWellFounded [IsWellFounded α r] [IsWellFounded β s] :
    IsWellFounded (α × β) (Prod.Lex r s) :=
  ⟨IsWellFounded.wf.prod_lex IsWellFounded.wf⟩

Well-foundedness of Lexicographic Product Relation

Informal description

For any types $\alpha$ and $\beta$ with well-founded relations $r$ and $s$ respectively, the lexicographic product relation $\mathrm{Prod.Lex}\,r\,s$ is well-founded on $\alpha \times \beta$.

instIsWellOrderProdLex instance

[IsWellOrder α r] [IsWellOrder β s] : IsWellOrder (α × β) (Prod.Lex r s)

Full source

instance [IsWellOrder α r] [IsWellOrder β s] : IsWellOrder (α × β) (Prod.Lex r s) where
  trichotomous := fun ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ =>
    match @trichotomous _ r _ a₁ b₁ with
    | Or.inl h₁ => Or.inl <| Prod.Lex.left _ _ h₁
    | Or.inr (Or.inr h₁) => Or.inr <| Or.inr <| Prod.Lex.left _ _ h₁
    | Or.inr (Or.inl (.refl _)) =>
        match @trichotomous _ s _ a₂ b₂ with
        | Or.inl h => Or.inl <| Prod.Lex.right _ h
        | Or.inr (Or.inr h) => Or.inr <| Or.inr <| Prod.Lex.right _ h
        | Or.inr (Or.inl (.refl _)) => Or.inr <| Or.inl rfl
  trans a b c h₁ h₂ := by
    rcases h₁ with ⟨a₂, b₂, ab⟩ | ⟨a₁, ab⟩ <;> rcases h₂ with ⟨c₁, c₂, bc⟩ | ⟨c₂, bc⟩
    exacts [.left _ _ (_root_.trans ab bc), .left _ _ ab, .left _ _ bc,
      .right _ (_root_.trans ab bc)]

Lexicographic Product of Well-orders is a Well-order

Informal description

For any types $\alpha$ and $\beta$ with well-order relations $r$ and $s$ respectively, the lexicographic product relation $\mathrm{Prod.Lex}\,r\,s$ is a well-order on $\alpha \times \beta$.

instIsWellFoundedInvImage instance

(r : α → α → Prop) [IsWellFounded α r] (f : β → α) : IsWellFounded _ (InvImage r f)

Full source

instance (r : α → α → Prop) [IsWellFounded α r] (f : β → α) : IsWellFounded _ (InvImage r f) :=
  ⟨InvImage.wf f IsWellFounded.wf⟩

Well-foundedness of Inverse Image Relation

Informal description

For any well-founded relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the inverse image relation on $\beta$ defined by $x \mapsto y \mapsto r (f x) (f y)$ is also well-founded.

instIsWellFoundedInvImageNatLt instance

(f : α → ℕ) : IsWellFounded _ (InvImage (· < ·) f)

Full source

instance (f : α → ℕ) : IsWellFounded _ (InvImage (· < ·) f) :=
  ⟨(measure f).wf⟩

Well-foundedness of the Inverse Image of the Natural Number Ordering

Informal description

For any function $f : \alpha \to \mathbb{N}$, the inverse image relation on $\alpha$ defined by $x \mapsto y \mapsto f(x) < f(y)$ is well-founded.

Subrelation.isWellFounded theorem

(r : α → α → Prop) [IsWellFounded α r] {s : α → α → Prop} (h : Subrelation s r) : IsWellFounded α s

Full source

theorem Subrelation.isWellFounded (r : α → α → Prop) [IsWellFounded α r] {s : α → α → Prop}
    (h : Subrelation s r) : IsWellFounded α s :=
  ⟨h.wf IsWellFounded.wf⟩

Well-foundedness is preserved under subrelations

Informal description

Let $r$ be a well-founded relation on a type $\alpha$, and let $s$ be a subrelation of $r$ (i.e., $s \subseteq r$). Then $s$ is also well-founded on $\alpha$.

Prod.wellFoundedLT' theorem

[PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] : WellFoundedLT (α × β)

Full source

/-- See `Prod.wellFoundedLT` for a version that only requires `Preorder α`. -/
theorem Prod.wellFoundedLT' [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] :
    WellFoundedLT (α × β) :=
  Subrelation.isWellFounded (Prod.Lex (· < ·) (· < ·))
    fun {x y} h ↦ (Prod.lt_iff.mp h).elim (fun h ↦ .left _ _ h.1)
    fun h ↦ h.1.lt_or_eq.elim (.left _ _) <| by cases x; cases y; rintro rfl; exact .right _ h.2

Well-foundedness of Strict Order on Product of Well-founded Partially Ordered and Preordered Types

Informal description

Let $\alpha$ be a partially ordered type with a well-founded strict less-than relation $<$, and let $\beta$ be a preordered type with a well-founded strict less-than relation $<$. Then the product type $\alpha \times \beta$ equipped with the strict less-than relation is also well-founded.

Prod.wellFoundedGT' theorem

[PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] : WellFoundedGT (α × β)

Full source

/-- See `Prod.wellFoundedGT` for a version that only requires `Preorder α`. -/
theorem Prod.wellFoundedGT' [PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] :
    WellFoundedGT (α × β) :=
  @Prod.wellFoundedLT' αᵒᵈ βᵒᵈ _ _ _ _

Well-foundedness of Strict Greater-Than Relation on Product of Well-founded Partially Ordered and Preordered Types

Informal description

Let $\alpha$ be a partially ordered type with a well-founded strict greater-than relation $>$, and let $\beta$ be a preordered type with a well-founded strict greater-than relation $>$. Then the product type $\alpha \times \beta$ equipped with the strict greater-than relation is also well-founded.

Set.Unbounded definition

(r : α → α → Prop) (s : Set α) : Prop

Full source

/-- An unbounded or cofinal set. -/
def Unbounded (r : α → α → Prop) (s : Set α) : Prop :=
  ∀ a, ∃ b ∈ s, ¬r b a

Unbounded set with respect to a relation

Informal description

A set $s$ in a type $\alpha$ is called *unbounded* with respect to a binary relation $r$ on $\alpha$ if for every element $a \in \alpha$, there exists an element $b \in s$ such that $\neg r(b, a)$. In other words, there is no upper bound for the set $s$ under the relation $r$.

Set.Bounded definition

(r : α → α → Prop) (s : Set α) : Prop

Full source

/-- A bounded or final set. Not to be confused with `Bornology.IsBounded`. -/
def Bounded (r : α → α → Prop) (s : Set α) : Prop :=
  ∃ a, ∀ b ∈ s, r b a

Bounded set with respect to a relation

Informal description

A set $s$ in a type $\alpha$ is called *bounded* with respect to a binary relation $r$ on $\alpha$ if there exists an element $a \in \alpha$ such that for every element $b \in s$, the relation $r(b, a)$ holds. In other words, there exists an upper bound $a$ for the set $s$ under the relation $r$.

Set.not_bounded_iff theorem

{r : α → α → Prop} (s : Set α) : ¬Bounded r s ↔ Unbounded r s

Full source

@[simp]
theorem not_bounded_iff {r : α → α → Prop} (s : Set α) : ¬Bounded r s¬Bounded r s ↔ Unbounded r s := by
  simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop, not_and, not_not]

Equivalence of Unboundedness and Non-Boundedness for Sets under a Relation

Informal description

For any binary relation $r$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ is not bounded with respect to $r$ if and only if it is unbounded with respect to $r$. In other words, $\neg \text{Bounded}(r, s) \leftrightarrow \text{Unbounded}(r, s)$.

Set.not_unbounded_iff theorem

{r : α → α → Prop} (s : Set α) : ¬Unbounded r s ↔ Bounded r s

Full source

@[simp]
theorem not_unbounded_iff {r : α → α → Prop} (s : Set α) : ¬Unbounded r s¬Unbounded r s ↔ Bounded r s := by
  rw [not_iff_comm, not_bounded_iff]

Equivalence of Boundedness and Non-Unboundedness for Sets under a Relation

Informal description

For any binary relation $r$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ is not unbounded with respect to $r$ if and only if it is bounded with respect to $r$. In other words, $\neg \text{Unbounded}(r, s) \leftrightarrow \text{Bounded}(r, s)$.

Set.unbounded_of_isEmpty theorem

[IsEmpty α] {r : α → α → Prop} (s : Set α) : Unbounded r s

Full source

theorem unbounded_of_isEmpty [IsEmpty α] {r : α → α → Prop} (s : Set α) : Unbounded r s :=
  isEmptyElim

Unboundedness of Sets in Empty Types

Informal description

For any empty type $\alpha$, any binary relation $r$ on $\alpha$, and any subset $s \subseteq \alpha$, the set $s$ is unbounded with respect to $r$.

Order.Preimage.instIsRefl instance

[IsRefl α r] {f : β → α} : IsRefl β (f ⁻¹'o r)

Full source

instance instIsRefl [IsRefl α r] {f : β → α} : IsRefl β (f ⁻¹'o r) :=
  ⟨fun _ => refl_of r _⟩

Reflexivity of Preimage Relation

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also reflexive. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsIrrefl instance

[IsIrrefl α r] {f : β → α} : IsIrrefl β (f ⁻¹'o r)

Full source

instance instIsIrrefl [IsIrrefl α r] {f : β → α} : IsIrrefl β (f ⁻¹'o r) :=
  ⟨fun _ => irrefl_of r _⟩

Irreflexivity of Preimage Relation

Informal description

For any irreflexive relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also irreflexive. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsSymm instance

[IsSymm α r] {f : β → α} : IsSymm β (f ⁻¹'o r)

Full source

instance instIsSymm [IsSymm α r] {f : β → α} : IsSymm β (f ⁻¹'o r) :=
  ⟨fun _ _ ↦ symm_of r⟩

Symmetry of Preimage Relation

Informal description

For any symmetric relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also symmetric. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsAsymm instance

[IsAsymm α r] {f : β → α} : IsAsymm β (f ⁻¹'o r)

Full source

instance instIsAsymm [IsAsymm α r] {f : β → α} : IsAsymm β (f ⁻¹'o r) :=
  ⟨fun _ _ ↦ asymm_of r⟩

Asymmetry of Preimage Relation

Informal description

For any asymmetric relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also asymmetric. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsTrans instance

[IsTrans α r] {f : β → α} : IsTrans β (f ⁻¹'o r)

Full source

instance instIsTrans [IsTrans α r] {f : β → α} : IsTrans β (f ⁻¹'o r) :=
  ⟨fun _ _ _ => trans_of r⟩

Transitivity of Preimage Relation

Informal description

For any transitive relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also transitive. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsPreorder instance

[IsPreorder α r] {f : β → α} : IsPreorder β (f ⁻¹'o r)

Full source

instance instIsPreorder [IsPreorder α r] {f : β → α} : IsPreorder β (f ⁻¹'o r) where

Preimage of a Preorder Relation is a Preorder

Informal description

For any preorder relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also a preorder. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsStrictOrder instance

[IsStrictOrder α r] {f : β → α} : IsStrictOrder β (f ⁻¹'o r)

Full source

instance instIsStrictOrder [IsStrictOrder α r] {f : β → α} : IsStrictOrder β (f ⁻¹'o r) where

Preimage of a Strict Order is a Strict Order

Informal description

For any strict order relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also a strict order. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsStrictWeakOrder instance

[IsStrictWeakOrder α r] {f : β → α} : IsStrictWeakOrder β (f ⁻¹'o r)

Full source

instance instIsStrictWeakOrder [IsStrictWeakOrder α r] {f : β → α} :
    IsStrictWeakOrder β (f ⁻¹'o r) where
  incomp_trans _ _ _ := IsStrictWeakOrder.incomp_trans (lt := r) _ _ _

Preimage of a Strict Weak Order is a Strict Weak Order

Informal description

For any strict weak order relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also a strict weak order. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsEquiv instance

[IsEquiv α r] {f : β → α} : IsEquiv β (f ⁻¹'o r)

Full source

instance instIsEquiv [IsEquiv α r] {f : β → α} : IsEquiv β (f ⁻¹'o r) where

Preimage of an Equivalence Relation is an Equivalence Relation

Informal description

For any equivalence relation $r$ on a type $\alpha$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also an equivalence relation. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y$ if and only if $f(x) r f(y)$.

Order.Preimage.instIsTotal instance

[IsTotal α r] {f : β → α} : IsTotal β (f ⁻¹'o r)

Full source

instance instIsTotal [IsTotal α r] {f : β → α} : IsTotal β (f ⁻¹'o r) :=
  ⟨fun _ _ => total_of r _ _⟩

Preimage of a Total Relation is Total

Informal description

For any type $\alpha$ with a total relation $r$ and any function $f : \beta \to \alpha$, the preimage relation $f^{-1}o r$ on $\beta$ is also total. Here, $f^{-1}o r$ is defined by $x (f^{-1}o r) y \leftrightarrow f(x) r f(y)$ for all $x, y \in \beta$.

Order.Preimage.isAntisymm theorem

[IsAntisymm α r] {f : β → α} (hf : f.Injective) : IsAntisymm β (f ⁻¹'o r)

Full source

theorem isAntisymm [IsAntisymm α r] {f : β → α} (hf : f.Injective) :
    IsAntisymm β (f ⁻¹'o r) :=
  ⟨fun _ _ h₁ h₂ ↦ hf <| antisymm_of r h₁ h₂⟩

Preimage of an Antisymmetric Relation under an Injective Function is Antisymmetric

Informal description

Let $\alpha$ be a type with an antisymmetric relation $r$, and let $f : \beta \to \alpha$ be an injective function. Then the preimage relation $f^{-1}o r$ on $\beta$, defined by $x (f^{-1}o r) y \leftrightarrow f(x) r f(y)$, is also antisymmetric.

IsNonstrictStrictOrder structure

(α : Type*) (r : semiOutParam (α → α → Prop)) (s : α → α → Prop)

Full source

/-- An unbundled relation class stating that `r` is the nonstrict relation corresponding to the
strict relation `s`. Compare `Preorder.lt_iff_le_not_le`. This is mostly meant to provide dot
notation on `(⊆)` and `(⊂)`. -/
class IsNonstrictStrictOrder (α : Type*) (r : semiOutParam (α → α → Prop)) (s : α → α → Prop) :
    Prop where
  /-- The relation `r` is the nonstrict relation corresponding to the strict relation `s`. -/
  right_iff_left_not_left (a b : α) : s a b ↔ r a b ∧ ¬r b a

Nonstrict-Strict Order Relation

Informal description

A structure that represents an unbundled relation class, stating that the relation `s` is the strict version of the nonstrict relation `r`. This means that for any elements `a` and `b` of type `α`, the relation `s a b` holds if and only if `r a b` holds and `r b a` does not hold. This is analogous to the relationship between `≤` and `<` in a preorder.

right_iff_left_not_left theorem

{r s : α → α → Prop} [IsNonstrictStrictOrder α r s] {a b : α} : s a b ↔ r a b ∧ ¬r b a

Full source

theorem right_iff_left_not_left {r s : α → α → Prop} [IsNonstrictStrictOrder α r s] {a b : α} :
    s a b ↔ r a b ∧ ¬r b a :=
  IsNonstrictStrictOrder.right_iff_left_not_left _ _

Characterization of Strict Relation in Nonstrict-Strict Order: $s(a, b) \leftrightarrow r(a, b) \land \neg r(b, a)$

Informal description

Let $\alpha$ be a type with relations $r$ and $s$ such that $s$ is the strict version of the nonstrict relation $r$. Then for any elements $a, b \in \alpha$, the relation $s(a, b)$ holds if and only if $r(a, b)$ holds and $r(b, a)$ does not hold.

right_iff_left_not_left_of theorem

(r s : α → α → Prop) [IsNonstrictStrictOrder α r s] {a b : α} : s a b ↔ r a b ∧ ¬r b a

Full source

/-- A version of `right_iff_left_not_left` with explicit `r` and `s`. -/
theorem right_iff_left_not_left_of (r s : α → α → Prop) [IsNonstrictStrictOrder α r s] {a b : α} :
    s a b ↔ r a b ∧ ¬r b a :=
  right_iff_left_not_left

Characterization of Strict Relation in Nonstrict-Strict Order: $s(a, b) \leftrightarrow r(a, b) \land \neg r(b, a)$

Informal description

Let $\alpha$ be a type equipped with relations $r$ and $s$, where $s$ is the strict version of the nonstrict relation $r$ (i.e., $[IsNonstrictStrictOrder\ \alpha\ r\ s]$). Then for any elements $a, b \in \alpha$, the relation $s(a, b)$ holds if and only if $r(a, b)$ holds and $r(b, a)$ does not hold, i.e., $$ s(a, b) \leftrightarrow r(a, b) \land \neg r(b, a). $$

instIsIrreflOfIsNonstrictStrictOrder instance

{s : α → α → Prop} [IsNonstrictStrictOrder α r s] : IsIrrefl α s

Full source

instance {s : α → α → Prop} [IsNonstrictStrictOrder α r s] : IsIrrefl α s :=
  ⟨fun _ h => ((right_iff_left_not_left_of r s).1 h).2 ((right_iff_left_not_left_of r s).1 h).1⟩

Irreflexivity of Strict Relation in Nonstrict-Strict Order

Informal description

For any type $\alpha$ with relations $r$ and $s$, if $s$ is the strict version of the nonstrict relation $r$ (i.e., $[IsNonstrictStrictOrder\ \alpha\ r\ s]$), then the relation $s$ is irreflexive. This means that for any element $a \in \alpha$, $s(a, a)$ does not hold.

subset_of_eq_of_subset theorem

(hab : a = b) (hbc : b ⊆ c) : a ⊆ c

Full source

lemma subset_of_eq_of_subset (hab : a = b) (hbc : b ⊆ c) : a ⊆ c := by rwa [hab]

Subset Preservation Under Equality

Informal description

For any elements $a$, $b$, and $c$ in a type $\alpha$ with a reflexive subset relation $\subseteq$, if $a = b$ and $b \subseteq c$, then $a \subseteq c$.

subset_of_subset_of_eq theorem

(hab : a ⊆ b) (hbc : b = c) : a ⊆ c

Full source

lemma subset_of_subset_of_eq (hab : a ⊆ b) (hbc : b = c) : a ⊆ c := by rwa [← hbc]

Subset Preservation Under Equality

Informal description

For any elements $a$, $b$, and $c$ in a type $\alpha$ equipped with a reflexive relation $\subseteq$, if $a \subseteq b$ and $b = c$, then $a \subseteq c$.

subset_refl theorem

[IsRefl α (· ⊆ ·)] (a : α) : a ⊆ a

Full source

@[refl, simp]
lemma subset_refl [IsRefl α (· ⊆ ·)] (a : α) : a ⊆ a := refl _

Reflexivity of the Subset Relation

Informal description

For any type $\alpha$ with a reflexive subset relation $\subseteq$, every element $a \in \alpha$ satisfies $a \subseteq a$.

subset_rfl theorem

[IsRefl α (· ⊆ ·)] : a ⊆ a

Full source

lemma subset_rfl [IsRefl α (· ⊆ ·)] : a ⊆ a := refl _

Reflexivity of Subset Relation

Informal description

For any set $a$ in a type $\alpha$ where the subset relation $\subseteq$ is reflexive, we have $a \subseteq a$.

subset_of_eq theorem

[IsRefl α (· ⊆ ·)] : a = b → a ⊆ b

Full source

lemma subset_of_eq [IsRefl α (· ⊆ ·)] : a = b → a ⊆ b := fun h => h ▸ subset_rfl

Subset Relation Preserves Equality: $a = b \to a \subseteq b$

Informal description

For any type $\alpha$ with a reflexive subset relation $\subseteq$, if two elements $a$ and $b$ are equal ($a = b$), then $a$ is a subset of $b$ ($a \subseteq b$).

superset_of_eq theorem

[IsRefl α (· ⊆ ·)] : a = b → b ⊆ a

Full source

lemma superset_of_eq [IsRefl α (· ⊆ ·)] : a = b → b ⊆ a := fun h => h ▸ subset_rfl

Superset Relation from Equality

Informal description

For any sets $a$ and $b$ in a type $\alpha$ where the subset relation $\subseteq$ is reflexive, if $a = b$ then $b \subseteq a$.

ne_of_not_subset theorem

[IsRefl α (· ⊆ ·)] : ¬a ⊆ b → a ≠ b

Full source

lemma ne_of_not_subset [IsRefl α (· ⊆ ·)] : ¬a ⊆ b → a ≠ b := mt subset_of_eq

Non-equality from Non-subset: $\neg(a \subseteq b) \implies a \neq b$

Informal description

For any type $\alpha$ with a reflexive subset relation $\subseteq$, if $a$ is not a subset of $b$, then $a$ is not equal to $b$.

ne_of_not_superset theorem

[IsRefl α (· ⊆ ·)] : ¬a ⊆ b → b ≠ a

Full source

lemma ne_of_not_superset [IsRefl α (· ⊆ ·)] : ¬a ⊆ b → b ≠ a := mt superset_of_eq

Non-equality from Non-superset: $\neg(a \subseteq b) \implies b \neq a$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ where the subset relation $\subseteq$ is reflexive, if $a$ is not a subset of $b$, then $b$ is not equal to $a$.

subset_trans theorem

[IsTrans α (· ⊆ ·)] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c

Full source

@[trans]
lemma subset_trans [IsTrans α (· ⊆ ·)] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c := _root_.trans

Transitivity of Subset Relation

Informal description

For any type $\alpha$ with a transitive subset relation $\subseteq$, and for any elements $a, b, c \in \alpha$, if $a \subseteq b$ and $b \subseteq c$, then $a \subseteq c$.

subset_antisymm theorem

[IsAntisymm α (· ⊆ ·)] : a ⊆ b → b ⊆ a → a = b

Full source

lemma subset_antisymm [IsAntisymm α (· ⊆ ·)] : a ⊆ b → b ⊆ a → a = b := antisymm

Antisymmetry of Subset Relation: $a \subseteq b \land b \subseteq a \implies a = b$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with an antisymmetric subset relation $\subseteq$, if $a \subseteq b$ and $b \subseteq a$, then $a = b$.

superset_antisymm theorem

[IsAntisymm α (· ⊆ ·)] : a ⊆ b → b ⊆ a → b = a

Full source

lemma superset_antisymm [IsAntisymm α (· ⊆ ·)] : a ⊆ b → b ⊆ a → b = a := antisymm'

Antisymmetry of Superset Relation: $a \subseteq b \land b \subseteq a \implies b = a$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with an antisymmetric subset relation $\subseteq$, if $a \subseteq b$ and $b \subseteq a$, then $b = a$.

subset_antisymm_iff theorem

[IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] : a = b ↔ a ⊆ b ∧ b ⊆ a

Full source

theorem subset_antisymm_iff [IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] : a = b ↔ a ⊆ b ∧ b ⊆ a :=
  ⟨fun h => ⟨h.subset', h.superset⟩, fun h => h.1.antisymm h.2⟩

Equivalence via Subset Antisymmetry: $a = b \leftrightarrow (a \subseteq b \land b \subseteq a)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with a reflexive and antisymmetric subset relation $\subseteq$, the equality $a = b$ holds if and only if both $a \subseteq b$ and $b \subseteq a$ hold.

superset_antisymm_iff theorem

[IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] : a = b ↔ b ⊆ a ∧ a ⊆ b

Full source

theorem superset_antisymm_iff [IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] : a = b ↔ b ⊆ a ∧ a ⊆ b :=
  ⟨fun h => ⟨h.superset, h.subset'⟩, fun h => h.1.antisymm' h.2⟩

Equivalence via Superset Antisymmetry: $a = b \leftrightarrow (b \supseteq a \land a \supseteq b)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with a reflexive and antisymmetric superset relation $\supseteq$, the equality $a = b$ holds if and only if both $b \supseteq a$ and $a \supseteq b$ hold.

ssubset_of_eq_of_ssubset theorem

(hab : a = b) (hbc : b ⊂ c) : a ⊂ c

Full source

lemma ssubset_of_eq_of_ssubset (hab : a = b) (hbc : b ⊂ c) : a ⊂ c := by rwa [hab]

Transitivity of Strict Subset Relation with Equality: $a = b \land b \subset c \Rightarrow a \subset c$

Informal description

For any elements $a, b, c$ of a type $\alpha$ with a strict subset relation $\subset$, if $a = b$ and $b \subset c$, then $a \subset c$.

ssubset_of_ssubset_of_eq theorem

(hab : a ⊂ b) (hbc : b = c) : a ⊂ c

Full source

lemma ssubset_of_ssubset_of_eq (hab : a ⊂ b) (hbc : b = c) : a ⊂ c := by rwa [← hbc]

Strict Subset Preservation Under Equality: $a \subset b \land b = c \implies a \subset c$

Informal description

For any elements $a$, $b$, and $c$ of a type $\alpha$ equipped with a strict subset relation $\subset$, if $a \subset b$ and $b = c$, then $a \subset c$.

ssubset_irrefl theorem

[IsIrrefl α (· ⊂ ·)] (a : α) : ¬a ⊂ a

Full source

lemma ssubset_irrefl [IsIrrefl α (· ⊂ ·)] (a : α) : ¬a ⊂ a := irrefl _

Irreflexivity of Strict Subset Relation

Informal description

For any element $a$ of type $\alpha$ where the strict subset relation $\subset$ is irreflexive, it is not the case that $a$ is a strict subset of itself, i.e., $\neg (a \subset a)$.

ssubset_irrfl theorem

[IsIrrefl α (· ⊂ ·)] {a : α} : ¬a ⊂ a

Full source

lemma ssubset_irrfl [IsIrrefl α (· ⊂ ·)] {a : α} : ¬a ⊂ a := irrefl _

Irreflexivity of Strict Subset Relation

Informal description

For any type $\alpha$ with an irreflexive strict subset relation $\subset$, and for any element $a$ of $\alpha$, it is not the case that $a$ is a strict subset of itself, i.e., $\neg(a \subset a)$.

ne_of_ssubset theorem

[IsIrrefl α (· ⊂ ·)] {a b : α} : a ⊂ b → a ≠ b

Full source

lemma ne_of_ssubset [IsIrrefl α (· ⊂ ·)] {a b : α} : a ⊂ b → a ≠ b := ne_of_irrefl

Strict Subset Implies Inequality

Informal description

For any type $\alpha$ with an irreflexive strict subset relation $\subset$, if $a \subset b$ for elements $a, b \in \alpha$, then $a \neq b$.

ne_of_ssuperset theorem

[IsIrrefl α (· ⊂ ·)] {a b : α} : a ⊂ b → b ≠ a

Full source

lemma ne_of_ssuperset [IsIrrefl α (· ⊂ ·)] {a b : α} : a ⊂ b → b ≠ a := ne_of_irrefl'

Strict Superset Implies Inequality: $a \subset b \Rightarrow b \neq a$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with an irreflexive strict subset relation $\subset$, if $a$ is a strict subset of $b$, then $b$ is not equal to $a$.

ssubset_trans theorem

[IsTrans α (· ⊂ ·)] {a b c : α} : a ⊂ b → b ⊂ c → a ⊂ c

Full source

@[trans]
lemma ssubset_trans [IsTrans α (· ⊂ ·)] {a b c : α} : a ⊂ b → b ⊂ c → a ⊂ c := _root_.trans

Transitivity of Strict Subset Relation

Informal description

For any elements $a$, $b$, and $c$ of a type $\alpha$ equipped with a transitive strict subset relation $\subset$, if $a \subset b$ and $b \subset c$, then $a \subset c$.

ssubset_asymm theorem

[IsAsymm α (· ⊂ ·)] {a b : α} : a ⊂ b → ¬b ⊂ a

Full source

lemma ssubset_asymm [IsAsymm α (· ⊂ ·)] {a b : α} : a ⊂ b → ¬b ⊂ a := asymm

Asymmetry of Strict Subset Relation

Informal description

For any type $\alpha$ with an asymmetric relation $\subset$, and for any elements $a, b \in \alpha$, if $a \subset b$ then it is not the case that $b \subset a$.

ssubset_iff_subset_not_subset theorem

: a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a

Full source

theorem ssubset_iff_subset_not_subset : a ⊂ ba ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a :=
  right_iff_left_not_left

Characterization of Strict Subset Relation: $a \subset b \leftrightarrow a \subseteq b \land \neg (b \subseteq a)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with subset relations $\subseteq$ and $\subset$, the strict subset relation $a \subset b$ holds if and only if the nonstrict subset relation $a \subseteq b$ holds and the reverse relation $b \subseteq a$ does not hold.

subset_of_ssubset theorem

(h : a ⊂ b) : a ⊆ b

Full source

theorem subset_of_ssubset (h : a ⊂ b) : a ⊆ b :=
  (ssubset_iff_subset_not_subset.1 h).1

Strict Subset Implies Nonstrict Subset

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with subset relations $\subseteq$ and $\subset$, if $a \subset b$ then $a \subseteq b$.

not_subset_of_ssubset theorem

(h : a ⊂ b) : ¬b ⊆ a

Full source

theorem not_subset_of_ssubset (h : a ⊂ b) : ¬b ⊆ a :=
  (ssubset_iff_subset_not_subset.1 h).2

Strict Subset Implies Non-Reversibility: $a \subset b \to \neg (b \subseteq a)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with subset relations $\subseteq$ and $\subset$, if $a \subset b$ then it is not the case that $b \subseteq a$.

not_ssubset_of_subset theorem

(h : a ⊆ b) : ¬b ⊂ a

Full source

theorem not_ssubset_of_subset (h : a ⊆ b) : ¬b ⊂ a := fun h' => not_subset_of_ssubset h' h

Nonstrict Subset Implies Non-Strict Reverse Subset: $a \subseteq b \to \neg (b \subset a)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with subset relations $\subseteq$ and $\subset$, if $a \subseteq b$ then it is not the case that $b \subset a$.

ssubset_of_subset_not_subset theorem

(h₁ : a ⊆ b) (h₂ : ¬b ⊆ a) : a ⊂ b

Full source

theorem ssubset_of_subset_not_subset (h₁ : a ⊆ b) (h₂ : ¬b ⊆ a) : a ⊂ b :=
  ssubset_iff_subset_not_subset.2 ⟨h₁, h₂⟩

Strict subset from nonstrict subset and non-reversibility: $a \subseteq b \land \neg (b \subseteq a) \to a \subset b$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with subset relations $\subseteq$ and $\subset$, if $a \subseteq b$ and it is not the case that $b \subseteq a$, then $a \subset b$.

ssubset_of_subset_of_ssubset theorem

[IsTrans α (· ⊆ ·)] (h₁ : a ⊆ b) (h₂ : b ⊂ c) : a ⊂ c

Full source

theorem ssubset_of_subset_of_ssubset [IsTrans α (· ⊆ ·)] (h₁ : a ⊆ b) (h₂ : b ⊂ c) : a ⊂ c :=
  (h₁.trans h₂.subset).ssubset_of_not_subset fun h => h₂.not_subset <| h.trans h₁

Transitivity of Strict Subset via Nonstrict Subset: $a \subseteq b \land b \subset c \to a \subset c$

Informal description

Let $\alpha$ be a type with a transitive subset relation $\subseteq$. For any elements $a, b, c \in \alpha$, if $a \subseteq b$ and $b \subset c$, then $a \subset c$.

ssubset_of_ssubset_of_subset theorem

[IsTrans α (· ⊆ ·)] (h₁ : a ⊂ b) (h₂ : b ⊆ c) : a ⊂ c

Full source

theorem ssubset_of_ssubset_of_subset [IsTrans α (· ⊆ ·)] (h₁ : a ⊂ b) (h₂ : b ⊆ c) : a ⊂ c :=
  (h₁.subset.trans h₂).ssubset_of_not_subset fun h => h₁.not_subset <| h₂.trans h

Transitivity of Strict Subset via Nonstrict Subset

Informal description

Let $\alpha$ be a type with a transitive subset relation $\subseteq$. For any elements $a, b, c \in \alpha$, if $a \subset b$ and $b \subseteq c$, then $a \subset c$.

ssubset_of_subset_of_ne theorem

[IsAntisymm α (· ⊆ ·)] (h₁ : a ⊆ b) (h₂ : a ≠ b) : a ⊂ b

Full source

theorem ssubset_of_subset_of_ne [IsAntisymm α (· ⊆ ·)] (h₁ : a ⊆ b) (h₂ : a ≠ b) : a ⊂ b :=
  h₁.ssubset_of_not_subset <| mt h₁.antisymm h₂

Strict Subset from Subset and Inequality under Antisymmetry

Informal description

Let $\alpha$ be a type with a subset relation $\subseteq$ that is antisymmetric. For any elements $a, b \in \alpha$, if $a \subseteq b$ and $a \neq b$, then $a \subset b$.

ssubset_of_ne_of_subset theorem

[IsAntisymm α (· ⊆ ·)] (h₁ : a ≠ b) (h₂ : a ⊆ b) : a ⊂ b

Full source

theorem ssubset_of_ne_of_subset [IsAntisymm α (· ⊆ ·)] (h₁ : a ≠ b) (h₂ : a ⊆ b) : a ⊂ b :=
  ssubset_of_subset_of_ne h₂ h₁

Strict Subset from Inequality and Subset under Antisymmetry

Informal description

Let $\alpha$ be a type with an antisymmetric subset relation $\subseteq$. For any elements $a, b \in \alpha$, if $a \neq b$ and $a \subseteq b$, then $a \subset b$.

ssubset_or_eq_of_subset theorem

[IsAntisymm α (· ⊆ ·)] (h : a ⊆ b) : a ⊂ b ∨ a = b

Full source

theorem ssubset_or_eq_of_subset [IsAntisymm α (· ⊆ ·)] (h : a ⊆ b) : a ⊂ ba ⊂ b ∨ a = b :=
  (eq_or_ssubset_of_subset h).symm

Subset Implies Strict Subset or Equality under Antisymmetry

Informal description

Let $\alpha$ be a type with a subset relation $\subseteq$ that is antisymmetric. For any elements $a$ and $b$ of type $\alpha$, if $a \subseteq b$, then either $a \subset b$ or $a = b$.

ssubset_iff_subset_ne theorem

[IsAntisymm α (· ⊆ ·)] : a ⊂ b ↔ a ⊆ b ∧ a ≠ b

Full source

theorem ssubset_iff_subset_ne [IsAntisymm α (· ⊆ ·)] : a ⊂ ba ⊂ b ↔ a ⊆ b ∧ a ≠ b :=
  ⟨fun h => ⟨h.subset, h.ne⟩, fun h => h.1.ssubset_of_ne h.2⟩

Strict Subset Characterization: $a \subset b \leftrightarrow (a \subseteq b \land a \neq b)$

Informal description

For any type $\alpha$ with an antisymmetric subset relation $\subseteq$, and for any elements $a, b \in \alpha$, the strict subset relation $a \subset b$ holds if and only if $a \subseteq b$ and $a \neq b$.

subset_iff_ssubset_or_eq theorem

[IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] : a ⊆ b ↔ a ⊂ b ∨ a = b

Full source

theorem subset_iff_ssubset_or_eq [IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] :
    a ⊆ ba ⊆ b ↔ a ⊂ b ∨ a = b :=
  ⟨fun h => h.ssubset_or_eq, fun h => h.elim subset_of_ssubset subset_of_eq⟩

Subset Equivalence: $a \subseteq b \leftrightarrow a \subset b \lor a = b$

Informal description

For any type $\alpha$ with a reflexive and antisymmetric subset relation $\subseteq$, and for any elements $a, b \in \alpha$, we have $a \subseteq b$ if and only if either $a \subset b$ or $a = b$.

instIsReflLe instance

[Preorder α] : IsRefl α (· ≤ ·)

Full source

instance [Preorder α] : IsRefl α (· ≤ ·) :=
  ⟨le_refl⟩

Reflexivity of $\leq$ in Preorders

Informal description

For any preorder $\alpha$, the relation $\leq$ is reflexive.

instIsReflGe instance

[Preorder α] : IsRefl α (· ≥ ·)

Full source

instance [Preorder α] : IsRefl α (· ≥ ·) :=
  IsRefl.swap _

Reflexivity of $\geq$ in Preorders

Informal description

For any preorder $\alpha$, the relation $\geq$ is reflexive.

instIsTransLe instance

[Preorder α] : IsTrans α (· ≤ ·)

Full source

instance [Preorder α] : IsTrans α (· ≤ ·) :=
  ⟨@le_trans _ _⟩

Transitivity of $\leq$ in Preorders

Informal description

For any preorder $\alpha$, the relation $\leq$ is transitive.

instIsTransGe instance

[Preorder α] : IsTrans α (· ≥ ·)

Full source

instance [Preorder α] : IsTrans α (· ≥ ·) :=
  IsTrans.swap _

Transitivity of $\geq$ in Preorders

Informal description

For any preorder $\alpha$, the relation $\geq$ is transitive.

instIsPreorderLe instance

[Preorder α] : IsPreorder α (· ≤ ·)

Full source

instance [Preorder α] : IsPreorder α (· ≤ ·) where

$\leq$ is a Preorder Relation in Preorders

Informal description

For any preorder $\alpha$, the relation $\leq$ is a preorder (i.e., it is reflexive and transitive).

instIsPreorderGe instance

[Preorder α] : IsPreorder α (· ≥ ·)

Full source

instance [Preorder α] : IsPreorder α (· ≥ ·) where

$\geq$ is a Preorder Relation in Preorders

Informal description

For any preorder $\alpha$, the relation $\geq$ is a preorder (i.e., it is reflexive and transitive).

instIsIrreflLt instance

[Preorder α] : IsIrrefl α (· < ·)

Full source

instance [Preorder α] : IsIrrefl α (· < ·) :=
  ⟨lt_irrefl⟩

Irreflexivity of Strict Order in Preorders

Informal description

For any preorder $\alpha$, the strict order relation $<$ is irreflexive, meaning that for all $x \in \alpha$, $x < x$ does not hold.

instIsIrreflGt instance

[Preorder α] : IsIrrefl α (· > ·)

Full source

instance [Preorder α] : IsIrrefl α (· > ·) :=
  IsIrrefl.swap _

Irreflexivity of Strict Greater-Than Relation in Preorders

Informal description

For any preorder $\alpha$, the strict greater-than relation $>$ is irreflexive, meaning that for all $x \in \alpha$, $x > x$ does not hold.

instIsTransLt instance

[Preorder α] : IsTrans α (· < ·)

Full source

instance [Preorder α] : IsTrans α (· < ·) :=
  ⟨@lt_trans _ _⟩

Transitivity of the Strict Order in a Preorder

Informal description

For any preorder $\alpha$, the strict less-than relation $<$ is transitive. That is, for any $a, b, c \in \alpha$, if $a < b$ and $b < c$, then $a < c$.

instIsTransGt instance

[Preorder α] : IsTrans α (· > ·)

Full source

instance [Preorder α] : IsTrans α (· > ·) :=
  IsTrans.swap _

Transitivity of the Strict Greater-Than Relation in Preorders

Informal description

For any preorder $\alpha$, the strict greater-than relation $>$ is transitive. That is, for any $a, b, c \in \alpha$, if $a > b$ and $b > c$, then $a > c$.

instIsAsymmLt instance

[Preorder α] : IsAsymm α (· < ·)

Full source

instance [Preorder α] : IsAsymm α (· < ·) :=
  ⟨@lt_asymm _ _⟩

Asymmetry of the Strict Order in a Preorder

Informal description

For any preorder $\alpha$, the strict less-than relation $<$ is asymmetric. That is, for any $x, y \in \alpha$, if $x < y$ then $\neg (y < x)$.

instIsAsymmGt instance

[Preorder α] : IsAsymm α (· > ·)

Full source

instance [Preorder α] : IsAsymm α (· > ·) :=
  IsAsymm.swap _

Asymmetry of the Strict Greater-Than Relation in Preorders

Informal description

For any preorder $\alpha$, the strict greater-than relation $>$ is asymmetric. That is, for any $x, y \in \alpha$, if $x > y$ then $\neg (y > x)$.

instIsAntisymmLt instance

[Preorder α] : IsAntisymm α (· < ·)

Full source

instance [Preorder α] : IsAntisymm α (· < ·) :=
  IsAsymm.isAntisymm _

Antisymmetry of the Strict Order in a Preorder

Informal description

For any preorder $\alpha$, the strict less-than relation $<$ is antisymmetric. That is, for any $x, y \in \alpha$, if $x < y$ and $y < x$ then $x = y$.

instIsAntisymmGt instance

[Preorder α] : IsAntisymm α (· > ·)

Full source

instance [Preorder α] : IsAntisymm α (· > ·) :=
  IsAsymm.isAntisymm _

Antisymmetry of the Strict Greater-Than Relation in Preorders

Informal description

For any preorder $\alpha$, the strict greater-than relation $>$ is antisymmetric. That is, for any $x, y \in \alpha$, if $x > y$ and $y > x$ then $x = y$.

instIsStrictOrderLt instance

[Preorder α] : IsStrictOrder α (· < ·)

Full source

instance [Preorder α] : IsStrictOrder α (· < ·) where

Strict Order Properties of $<$ in Preorders

Informal description

For any preorder $\alpha$, the strict less-than relation $<$ is a strict order, meaning it is both irreflexive and transitive.

instIsStrictOrderGt instance

[Preorder α] : IsStrictOrder α (· > ·)

Full source

instance [Preorder α] : IsStrictOrder α (· > ·) where

Strict Order Properties of $>$ in Preorders

Informal description

For any preorder $\alpha$, the strict greater-than relation $>$ is a strict order, meaning it is both irreflexive and transitive.

instIsNonstrictStrictOrderLeLt instance

[Preorder α] : IsNonstrictStrictOrder α (· ≤ ·) (· < ·)

Full source

instance [Preorder α] : IsNonstrictStrictOrder α (· ≤ ·) (· < ·) :=
  ⟨@lt_iff_le_not_le _ _⟩

Strict Order Relation from Preorder

Informal description

For any preorder $\alpha$, the relation $<$ is the strict version of the nonstrict relation $\leq$. That is, for any elements $a$ and $b$ in $\alpha$, we have $a < b$ if and only if $a \leq b$ and $b \nleq a$.

instIsAntisymmLe instance

[PartialOrder α] : IsAntisymm α (· ≤ ·)

Full source

instance [PartialOrder α] : IsAntisymm α (· ≤ ·) :=
  ⟨@le_antisymm _ _⟩

Antisymmetry of $\leq$ in Partial Orders

Informal description

For any partially ordered type $\alpha$, the relation $\leq$ is antisymmetric.

instIsAntisymmGe instance

[PartialOrder α] : IsAntisymm α (· ≥ ·)

Full source

instance [PartialOrder α] : IsAntisymm α (· ≥ ·) :=
  IsAntisymm.swap _

Antisymmetry of $\geq$ in Partial Orders

Informal description

For any partially ordered type $\alpha$, the relation $\geq$ is antisymmetric.

instIsPartialOrderLe instance

[PartialOrder α] : IsPartialOrder α (· ≤ ·)

Full source

instance [PartialOrder α] : IsPartialOrder α (· ≤ ·) where

$\leq$ is a Partial Order Relation in Partial Orders

Informal description

For any partially ordered type $\alpha$, the relation $\leq$ is a partial order (i.e., it is reflexive, transitive, and antisymmetric).

instIsPartialOrderGe instance

[PartialOrder α] : IsPartialOrder α (· ≥ ·)

Full source

instance [PartialOrder α] : IsPartialOrder α (· ≥ ·) where

$\geq$ is a Partial Order Relation in Partial Orders

Informal description

For any partially ordered type $\alpha$, the relation $\geq$ is a partial order (i.e., it is reflexive, transitive, and antisymmetric).

LE.isTotal instance

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

Full source

instance LE.isTotal [LinearOrder α] : IsTotal α (· ≤ ·) :=
  ⟨le_total⟩

Totality of $\leq$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the relation $\leq$ is a total relation. That is, for any two elements $x$ and $y$ in $\alpha$, either $x \leq y$ or $y \leq x$ holds.

instIsTotalGe instance

[LinearOrder α] : IsTotal α (· ≥ ·)

Full source

instance [LinearOrder α] : IsTotal α (· ≥ ·) :=
  IsTotal.swap _

Totality of $\geq$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the relation $\geq$ is a total relation. That is, for any two elements $x$ and $y$ in $\alpha$, either $x \geq y$ or $y \geq x$ holds.

instIsLinearOrderLe instance

[LinearOrder α] : IsLinearOrder α (· ≤ ·)

Full source

instance [LinearOrder α] : IsLinearOrder α (· ≤ ·) where

$\leq$ is a Linear Order Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the relation $\leq$ is a linear order (i.e., it is reflexive, transitive, antisymmetric, and total).

instIsLinearOrderGe instance

[LinearOrder α] : IsLinearOrder α (· ≥ ·)

Full source

instance [LinearOrder α] : IsLinearOrder α (· ≥ ·) where

$\geq$ is a Linear Order Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the relation $\geq$ is a linear order (i.e., it is reflexive, transitive, antisymmetric, and total).

instIsTrichotomousLt instance

[LinearOrder α] : IsTrichotomous α (· < ·)

Full source

instance [LinearOrder α] : IsTrichotomous α (· < ·) :=
  ⟨lt_trichotomy⟩

Trichotomy of Strict Order in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the strict less-than relation $<$ is trichotomous, meaning that for any two elements $x$ and $y$ in $\alpha$, exactly one of the following holds: $x < y$, $x = y$, or $y < x$.

instIsTrichotomousGt instance

[LinearOrder α] : IsTrichotomous α (· > ·)

Full source

instance [LinearOrder α] : IsTrichotomous α (· > ·) :=
  IsTrichotomous.swap _

Trichotomy of Strict Greater-Than Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the strict greater-than relation $>$ is trichotomous, meaning that for any two elements $x$ and $y$ in $\alpha$, exactly one of the following holds: $x > y$, $x = y$, or $y > x$.

instIsTrichotomousLe instance

[LinearOrder α] : IsTrichotomous α (· ≤ ·)

Full source

instance [LinearOrder α] : IsTrichotomous α (· ≤ ·) :=
  IsTotal.isTrichotomous _

Trichotomy of $\leq$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the relation $\leq$ is trichotomous. That is, for any two elements $x$ and $y$ in $\alpha$, exactly one of the following holds: $x < y$, $x = y$, or $y < x$.

instIsTrichotomousGe instance

[LinearOrder α] : IsTrichotomous α (· ≥ ·)

Full source

instance [LinearOrder α] : IsTrichotomous α (· ≥ ·) :=
  IsTotal.isTrichotomous _

Trichotomy of $\geq$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the relation $\geq$ is trichotomous. That is, for any two elements $x$ and $y$ in $\alpha$, exactly one of the following holds: $x > y$, $x = y$, or $y > x$.

instIsStrictTotalOrderLt instance

[LinearOrder α] : IsStrictTotalOrder α (· < ·)

Full source

instance [LinearOrder α] : IsStrictTotalOrder α (· < ·) where

Strict Total Order Properties of $<$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the strict less-than relation $<$ is a strict total order, meaning it is irreflexive, transitive, and trichotomous.

instIsOrderConnectedLt instance

[LinearOrder α] : IsOrderConnected α (· < ·)

Full source

instance [LinearOrder α] : IsOrderConnected α (· < ·) := by infer_instance

Order Connectedness of $<$ in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the strict less-than relation $<$ is order connected. This means that for any elements $a, b, c \in \alpha$, if $a < c$ then either $a < b$ or $b < c$.

transitive_le theorem

[Preorder α] : Transitive (@LE.le α _)

Full source

theorem transitive_le [Preorder α] : Transitive (@LE.le α _) :=
  transitive_of_trans _

Transitivity of $\leq$ in Preorders

Informal description

For any preorder $\alpha$, the relation $\leq$ is transitive, meaning that for any elements $x, y, z \in \alpha$, if $x \leq y$ and $y \leq z$, then $x \leq z$.

transitive_lt theorem

[Preorder α] : Transitive (@LT.lt α _)

Full source

theorem transitive_lt [Preorder α] : Transitive (@LT.lt α _) :=
  transitive_of_trans _

Transitivity of Strict Order in Preorders

Informal description

For any preorder $\alpha$, the strict less-than relation $<$ is transitive. That is, for any $a, b, c \in \alpha$, if $a < b$ and $b < c$, then $a < c$.

transitive_ge theorem

[Preorder α] : Transitive (@GE.ge α _)

Full source

theorem transitive_ge [Preorder α] : Transitive (@GE.ge α _) :=
  transitive_of_trans _

Transitivity of $\geq$ in Preorders

Informal description

For any preorder $\alpha$, the relation $\geq$ is transitive, meaning that for any elements $x, y, z \in \alpha$, if $x \geq y$ and $y \geq z$, then $x \geq z$.

transitive_gt theorem

[Preorder α] : Transitive (@GT.gt α _)

Full source

theorem transitive_gt [Preorder α] : Transitive (@GT.gt α _) :=
  transitive_of_trans _

Transitivity of Strict Greater-Than Relation in Preorders

Informal description

For any preorder $\alpha$, the strict greater-than relation $>$ is transitive. That is, for any $a, b, c \in \alpha$, if $a > b$ and $b > c$, then $a > c$.

OrderDual.isTotal_le instance

[LE α] [h : IsTotal α (· ≤ ·)] : IsTotal αᵒᵈ (· ≤ ·)

Full source

instance OrderDual.isTotal_le [LE α] [h : IsTotal α (· ≤ ·)] : IsTotal αᵒᵈ (· ≤ ·) :=
  @IsTotal.swap α _ h

Total Order Property Preserved Under Order Duality

Informal description

For any type $\alpha$ with a total order relation $\leq$, the dual order relation $\leq$ on the order dual $\alpha^\text{op}$ is also total.

instWellFoundedLTNat instance

: WellFoundedLT ℕ

Full source

instance : WellFoundedLT ℕ :=
  ⟨Nat.lt_wfRel.wf⟩

Well-foundedness of the Strict Order on Natural Numbers

Informal description

The strict less-than relation $<$ on the natural numbers $\mathbb{N}$ is well-founded.

isWellOrder_lt instance

[LinearOrder α] [WellFoundedLT α] : IsWellOrder α (· < ·)

Full source

instance (priority := 100) isWellOrder_lt [LinearOrder α] [WellFoundedLT α] :
    IsWellOrder α (· < ·) where

Well-ordering from Well-founded Strict Order in Linear Orders

Informal description

For any linearly ordered type $\alpha$ with a well-founded strict less-than relation $<$, the relation $<$ is a well-order on $\alpha$.

isWellOrder_gt instance

[LinearOrder α] [WellFoundedGT α] : IsWellOrder α (· > ·)

Full source

instance (priority := 100) isWellOrder_gt [LinearOrder α] [WellFoundedGT α] :
    IsWellOrder α (· > ·) where

Well-ordering from Well-founded Strict Greater-Than Relation in Linear Orders

Informal description

For any linearly ordered type $\alpha$ with a well-founded strict greater-than relation $>$, the relation $>$ is a well-order on $\alpha$.