doc-next-gen

Mathlib.Order.Defs.Unbundled

Module docstring

{"# Orders

Defines classes for preorders, partial orders, and linear orders and proves some basic lemmas about them. ","### Unbundled classes ","### Minimal and maximal ","### Upper and lower sets "}

EmptyRelation definition
{α : Sort*}
Full source 
/-- An empty relation does not relate any elements. -/
@[nolint unusedArguments] def EmptyRelation {α : Sort*} := fun _ _ : α ↦ False
Empty Relation
Informal description
The empty relation on a type $\alpha$ is the relation that does not relate any two elements of $\alpha$. Formally, for any $x, y \in \alpha$, the relation $\text{EmptyRelation}(x, y)$ is always false.
IsIrrefl structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsIrrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
holds). -/
class IsIrrefl (α : Sort*) (r : α → α → Prop) : Prop where
  irrefl : ∀ a, ¬r a a
Irreflexive Relation
Informal description
A binary relation `r` on a type `α` is called *irreflexive* if for every element `x` of `α`, the relation `r x x` does not hold. In other words, no element is related to itself under `r`.
IsRefl structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsRefl X r` means the binary relation `r` on `X` is reflexive. -/
class IsRefl (α : Sort*) (r : α → α → Prop) : Prop where
  refl : ∀ a, r a a
Reflexive binary relation
Informal description
The structure `IsRefl X r` asserts that the binary relation `r` on the type `X` is reflexive, meaning that for every element `x` in `X`, the relation `r x x` holds.
IsSymm structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsSymm X r` means the binary relation `r` on `X` is symmetric. -/
class IsSymm (α : Sort*) (r : α → α → Prop) : Prop where
  symm : ∀ a b, r a b → r b a
Symmetric Binary Relation
Informal description
The structure `IsSymm X r` asserts that the binary relation `r` on a type `X` is symmetric, meaning that for any two elements `x` and `y` in `X`, if `r x y` holds, then `r y x` also holds.
IsAsymm structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsAsymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
`r a b → ¬ r b a`. -/
class IsAsymm (α : Sort*) (r : α → α → Prop) : Prop where
  asymm : ∀ a b, r a b → ¬r b a
Asymmetric relation
Informal description
A binary relation \( r \) on a type \( \alpha \) is called *asymmetric* if for any elements \( a, b \in \alpha \), \( r(a, b) \) implies \( \neg r(b, a) \).
IsAntisymm structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsAntisymm X r` means the binary relation `r` on `X` is antisymmetric. -/
class IsAntisymm (α : Sort*) (r : α → α → Prop) : Prop where
  antisymm : ∀ a b, r a b → r b a → a = b
Antisymmetric Relation
Informal description
The structure `IsAntisymm X r` asserts that the binary relation `r` on the type `X` is antisymmetric, meaning that for any two elements `x` and `y` in `X`, if both `r x y` and `r y x` hold, then `x = y`.
IsAsymm.toIsAntisymm instance
{α : Sort*} (r : α → α → Prop) [IsAsymm α r] : IsAntisymm α r
Full source 
instance (priority := 100) IsAsymm.toIsAntisymm {α : Sort*} (r : α → α → Prop) [IsAsymm α r] :
    IsAntisymm α r where
  antisymm _ _ hx hy := (IsAsymm.asymm _ _ hx hy).elim
Asymmetric Relations are Antisymmetric
Informal description
For any type $\alpha$ and binary relation $r$ on $\alpha$, if $r$ is asymmetric, then $r$ is also antisymmetric.
IsTrans structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsTrans X r` means the binary relation `r` on `X` is transitive. -/
class IsTrans (α : Sort*) (r : α → α → Prop) : Prop where
  trans : ∀ a b c, r a b → r b c → r a c
Transitive binary relation
Informal description
The structure `IsTrans X r` asserts that the binary relation `r` on the type `X` is transitive, meaning that for any elements `x`, `y`, `z` in `X`, if `r x y` and `r y z` hold, then `r x z` must also hold.
instTransOfIsTrans instance
{α : Sort*} {r : α → α → Prop} [IsTrans α r] : Trans r r r
Full source 
instance {α : Sort*} {r : α → α → Prop} [IsTrans α r] : Trans r r r :=
  ⟨IsTrans.trans _ _ _⟩
Transitivity of a Binary Relation
Informal description
For any type $\alpha$ and transitive binary relation $r$ on $\alpha$, the relation $r$ satisfies the transitivity property: if $r(x, y)$ and $r(y, z)$ hold, then $r(x, z)$ holds.
instIsTransOfTrans instance
{α : Sort*} {r : α → α → Prop} [Trans r r r] : IsTrans α r
Full source 
instance (priority := 100) {α : Sort*} {r : α → α → Prop} [Trans r r r] : IsTrans α r :=
  ⟨fun _ _ _ => Trans.trans⟩
Transitive Relations from Trans Typeclass
Informal description
For any type $\alpha$ and binary relation $r$ on $\alpha$, if $r$ is transitive (i.e., satisfies the `Trans` typeclass), then $r$ is a transitive relation (i.e., satisfies the `IsTrans` structure).
IsTotal structure
(α : Sort*) (r : α → α → Prop)
Full source 
/-- `IsTotal X r` means that the binary relation `r` on `X` is total, that is, that for any
`x y : X` we have `r x y` or `r y x`. -/
class IsTotal (α : Sort*) (r : α → α → Prop) : Prop where
  total : ∀ a b, r a b ∨ r b a
Total binary relation
Informal description
The structure `IsTotal X r` asserts that the binary relation `r` on a type `X` is total, meaning that for any two elements `x` and `y` in `X`, either `r x y` holds or `r y x` holds.
IsPreorder structure
(α : Sort*) (r : α → α → Prop) : Prop extends IsRefl α r, IsTrans α r
Full source 
/-- `IsPreorder X r` means that the binary relation `r` on `X` is a pre-order, that is, reflexive
and transitive. -/
class IsPreorder (α : Sort*) (r : α → α → Prop) : Prop extends IsRefl α r, IsTrans α r
Preorder Relation
Informal description
A binary relation `r` on a type `α` is called a *preorder* if it is reflexive (i.e., `r x x` holds for all `x ∈ α`) and transitive (i.e., `r x y` and `r y z` imply `r x z` for all `x, y, z ∈ α`).
IsPartialOrder structure
(α : Sort*) (r : α → α → Prop) : Prop extends IsPreorder α r, IsAntisymm α r
Full source 
/-- `IsPartialOrder X r` means that the binary relation `r` on `X` is a partial order, that is,
`IsPreorder X r` and `IsAntisymm X r`. -/
class IsPartialOrder (α : Sort*) (r : α → α → Prop) : Prop extends IsPreorder α r, IsAntisymm α r
Partial Order Structure
Informal description
The structure `IsPartialOrder X r` asserts that the binary relation `r` on a type `X` is a partial order, meaning it satisfies reflexivity, transitivity, and antisymmetry. Specifically: 1. **Reflexivity**: For every $x \in X$, $r(x, x)$ holds. 2. **Transitivity**: For any $x, y, z \in X$, if $r(x, y)$ and $r(y, z)$ hold, then $r(x, z)$ holds. 3. **Antisymmetry**: For any $x, y \in X$, if both $r(x, y)$ and $r(y, x)$ hold, then $x = y$.
IsLinearOrder structure
(α : Sort*) (r : α → α → Prop) : Prop extends IsPartialOrder α r, IsTotal α r
Full source 
/-- `IsLinearOrder X r` means that the binary relation `r` on `X` is a linear order, that is,
`IsPartialOrder X r` and `IsTotal X r`. -/
class IsLinearOrder (α : Sort*) (r : α → α → Prop) : Prop extends IsPartialOrder α r, IsTotal α r
Linear Order Structure
Informal description
The structure `IsLinearOrder α r` asserts that the binary relation `r` on a type `α` is a linear order, meaning it satisfies the properties of a partial order (reflexivity, transitivity, and antisymmetry) and is total (any two elements are comparable).
IsEquiv structure
(α : Sort*) (r : α → α → Prop) : Prop extends IsPreorder α r, IsSymm α r
Full source 
/-- `IsEquiv X r` means that the binary relation `r` on `X` is an equivalence relation, that
is, `IsPreorder X r` and `IsSymm X r`. -/
class IsEquiv (α : Sort*) (r : α → α → Prop) : Prop extends IsPreorder α r, IsSymm α r
Equivalence Relation
Informal description
A binary relation `r` on a type `α` is an equivalence relation if it is reflexive, transitive (i.e., a preorder), and symmetric. In other words, for all `x, y, z : α`, the following hold: 1. Reflexivity: `r x x` 2. Transitivity: `r x y` and `r y z` implies `r x z` 3. Symmetry: `r x y` implies `r y x`
IsStrictOrder structure
(α : Sort*) (r : α → α → Prop) : Prop extends IsIrrefl α r, IsTrans α r
Full source 
/-- `IsStrictOrder X r` means that the binary relation `r` on `X` is a strict order, that is,
`IsIrrefl X r` and `IsTrans X r`. -/
class IsStrictOrder (α : Sort*) (r : α → α → Prop) : Prop extends IsIrrefl α r, IsTrans α r
Strict Order Relation
Informal description
A binary relation `r` on a type `α` is called a strict order if it is both irreflexive (no element is related to itself) and transitive (if `x` is related to `y` and `y` is related to `z`, then `x` is related to `z`).
IsStrictWeakOrder structure
(α : Sort*) (lt : α → α → Prop) : Prop extends IsStrictOrder α lt
Full source 
/-- `IsStrictWeakOrder X lt` means that the binary relation `lt` on `X` is a strict weak order,
that is, `IsStrictOrder X lt` and `¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a`. -/
class IsStrictWeakOrder (α : Sort*) (lt : α → α → Prop) : Prop extends IsStrictOrder α lt where
  incomp_trans : ∀ a b c, ¬lt a b¬lt a b ∧ ¬lt b a → ¬lt b c¬lt b c ∧ ¬lt c b → ¬lt a c¬lt a c ∧ ¬lt c a
Strict weak order
Informal description
A binary relation `lt` on a type `α` is called a strict weak order if it is a strict order (irreflexive and transitive) and satisfies the following condition: for any elements `a`, `b`, and `c` in `α`, if neither `lt a b` nor `lt b a` holds, and neither `lt b c` nor `lt c b` holds, then neither `lt a c` nor `lt c a` holds. This condition ensures that the incomparability relation induced by `lt` is transitive.
IsTrichotomous structure
(α : Sort*) (lt : α → α → Prop)
Full source 
/-- `IsTrichotomous X lt` means that the binary relation `lt` on `X` is trichotomous, that is,
either `lt a b` or `a = b` or `lt b a` for any `a` and `b`. -/
class IsTrichotomous (α : Sort*) (lt : α → α → Prop) : Prop where
  trichotomous : ∀ a b, lt a b ∨ a = b ∨ lt b a
Trichotomous relation
Informal description
A binary relation `lt` on a type `α` is called *trichotomous* if for any two elements `a` and `b` in `α`, exactly one of the following holds: `lt a b`, `a = b`, or `lt b a`.
IsStrictTotalOrder structure
(α : Sort*) (lt : α → α → Prop) : Prop extends IsTrichotomous α lt, IsStrictOrder α lt
Full source 
/-- `IsStrictTotalOrder X lt` means that the binary relation `lt` on `X` is a strict total order,
that is, `IsTrichotomous X lt` and `IsStrictOrder X lt`. -/
class IsStrictTotalOrder (α : Sort*) (lt : α → α → Prop) : Prop
    extends IsTrichotomous α lt, IsStrictOrder α lt
Strict total order
Informal description
A binary relation `lt` on a type `α` is a strict total order if it satisfies the following properties: 1. Trichotomy: For any two elements `x` and `y` in `α`, exactly one of the following holds: `lt x y`, `x = y`, or `lt y x`. 2. Strict order: The relation `lt` is irreflexive (no element is related to itself) and transitive (if `lt x y` and `lt y z`, then `lt x z`).
iff_isEquiv instance
: IsEquiv Prop Iff
Full source 
/-- `Iff` is an equivalence relation. -/
instance iff_isEquiv : IsEquiv Prop Iff where
  symm := @Iff.symm
  trans := @Iff.trans
  refl := @Iff.refl
Logical Equivalence is an Equivalence Relation
Informal description
The logical equivalence relation `Iff` on propositions is an equivalence relation. That is, for any propositions `P`, `Q`, `R`: 1. Reflexivity: `P ↔ P` 2. Symmetry: `P ↔ Q` implies `Q ↔ P` 3. Transitivity: `P ↔ Q` and `Q ↔ R` implies `P ↔ R`
irrefl theorem
[IsIrrefl α r] (a : α) : ¬a ≺ a
Full source 
lemma irrefl [IsIrrefl α r] (a : α) : ¬a ≺ a := IsIrrefl.irrefl a
Irreflexivity Property of a Binary Relation
Informal description
For any irreflexive binary relation $\prec$ on a type $\alpha$ and any element $a \in \alpha$, the relation $a \prec a$ does not hold.
refl theorem
[IsRefl α r] (a : α) : a ≺ a
Full source 
lemma refl [IsRefl α r] (a : α) : a ≺ a := IsRefl.refl a
Reflexivity of a Binary Relation
Informal description
For any reflexive binary relation $\prec$ on a type $\alpha$ and any element $a \in \alpha$, we have $a \prec a$.
trans theorem
[IsTrans α r] : a ≺ b → b ≺ c → a ≺ c
Full source 
lemma trans [IsTrans α r] : a ≺ b → b ≺ c → a ≺ c := IsTrans.trans _ _ _
Transitivity Property: $a \prec b \land b \prec c \implies a \prec c$
Informal description
For any transitive binary relation $\prec$ on a type $\alpha$ and any elements $a, b, c \in \alpha$, if $a \prec b$ and $b \prec c$ hold, then $a \prec c$ also holds.
symm theorem
[IsSymm α r] : a ≺ b → b ≺ a
Full source 
lemma symm [IsSymm α r] : a ≺ b → b ≺ a := IsSymm.symm _ _
Symmetry Property: $a \prec b \implies b \prec a$
Informal description
For any symmetric binary relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a \prec b$ holds, then $b \prec a$ also holds.
antisymm theorem
[IsAntisymm α r] : a ≺ b → b ≺ a → a = b
Full source 
lemma antisymm [IsAntisymm α r] : a ≺ b → b ≺ a → a = b := IsAntisymm.antisymm _ _
Antisymmetry of a Relation: `a ≺ b ∧ b ≺ a → a = b`
Informal description
For any binary relation `≺` on a type `α` that is antisymmetric, if `a ≺ b` and `b ≺ a` hold for some elements `a, b ∈ α`, then `a = b`.
asymm theorem
[IsAsymm α r] : a ≺ b → ¬b ≺ a
Full source 
lemma asymm [IsAsymm α r] : a ≺ b → ¬b ≺ a := IsAsymm.asymm _ _
Asymmetry Property: $a \prec b \implies \neg(b \prec a)$
Informal description
For any binary relation $\prec$ on a type $\alpha$ that is asymmetric, if $a \prec b$ holds for some elements $a, b \in \alpha$, then $b \prec a$ does not hold.
trichotomous theorem
[IsTrichotomous α r] : ∀ a b : α, a ≺ b ∨ a = b ∨ b ≺ a
Full source 
lemma trichotomous [IsTrichotomous α r] : ∀ a b : α, a ≺ b ∨ a = b ∨ b ≺ a :=
  IsTrichotomous.trichotomous
Trichotomy Property: $a \prec b \lor a = b \lor b \prec a$
Informal description
For any binary relation $\prec$ on a type $\alpha$ that is trichotomous, and for any elements $a, b \in \alpha$, exactly one of the following holds: $a \prec b$, $a = b$, or $b \prec a$.
IsIrrefl.decide instance
[DecidableRel r] [IsIrrefl α r] : IsIrrefl α (fun a b => decide (r a b) = true)
Full source 
instance IsIrrefl.decide [DecidableRel r] [IsIrrefl α r] :
    IsIrrefl α (fun a b => decide (r a b) = true) where
  irrefl := fun a => by simpa using irrefl a
Irreflexivity Preservation under Decidable Relation Lifting
Informal description
For any type $\alpha$ with a decidable binary relation $r$ that is irreflexive, the relation defined by $\lambda a b, \text{decide}(r a b) = \text{true}$ is also irreflexive.
IsRefl.decide instance
[DecidableRel r] [IsRefl α r] : IsRefl α (fun a b => decide (r a b) = true)
Full source 
instance IsRefl.decide [DecidableRel r] [IsRefl α r] :
    IsRefl α (fun a b => decide (r a b) = true) where
  refl := fun a => by simpa using refl a
Reflexivity Preservation under Decidable Relation Lifting
Informal description
For any type $\alpha$ with a decidable binary relation $r$ that is reflexive, the relation defined by $\lambda a b, \text{decide}(r a b) = \text{true}$ is also reflexive.
IsTrans.decide instance
[DecidableRel r] [IsTrans α r] : IsTrans α (fun a b => decide (r a b) = true)
Full source 
instance IsTrans.decide [DecidableRel r] [IsTrans α r] :
    IsTrans α (fun a b => decide (r a b) = true) where
  trans := fun a b c => by simpa using trans a b c
Transitivity Preservation under Decidable Relation Lifting
Informal description
For any type $\alpha$ with a decidable binary relation $r$ that is transitive, the relation defined by $\lambda a b, \text{decide}(r a b) = \text{true}$ is also transitive.
IsSymm.decide instance
[DecidableRel r] [IsSymm α r] : IsSymm α (fun a b => decide (r a b) = true)
Full source 
instance IsSymm.decide [DecidableRel r] [IsSymm α r] :
    IsSymm α (fun a b => decide (r a b) = true) where
  symm := fun a b => by simpa using symm a b
Decidable Symmetric Relation Preserves Symmetry
Informal description
For any type $\alpha$ with a decidable symmetric relation $r$, the relation defined by $(a, b) \mapsto \text{decide}(r(a, b)) = \text{true}$ is also symmetric.
IsAntisymm.decide instance
[DecidableRel r] [IsAntisymm α r] : IsAntisymm α (fun a b => decide (r a b) = true)
Full source 
instance IsAntisymm.decide [DecidableRel r] [IsAntisymm α r] :
    IsAntisymm α (fun a b => decide (r a b) = true) where
  antisymm a b h₁ h₂ := antisymm (r := r) _ _ (by simpa using h₁) (by simpa using h₂)
Decidable Antisymmetric Relation Preserves Antisymmetry
Informal description
For any type $\alpha$ with a decidable antisymmetric relation $r$, the relation defined by $(a, b) \mapsto \text{decide}(r(a, b)) = \text{true}$ is also antisymmetric.
IsAsymm.decide instance
[DecidableRel r] [IsAsymm α r] : IsAsymm α (fun a b => decide (r a b) = true)
Full source 
instance IsAsymm.decide [DecidableRel r] [IsAsymm α r] :
    IsAsymm α (fun a b => decide (r a b) = true) where
  asymm := fun a b => by simpa using asymm a b
Decidable Asymmetric Relation Preserves Asymmetry
Informal description
For any type $\alpha$ with a decidable asymmetric relation $r$, the relation defined by $(a, b) \mapsto \text{decide}(r(a, b)) = \text{true}$ is also asymmetric.
IsTotal.decide instance
[DecidableRel r] [IsTotal α r] : IsTotal α (fun a b => decide (r a b) = true)
Full source 
instance IsTotal.decide [DecidableRel r] [IsTotal α r] :
    IsTotal α (fun a b => decide (r a b) = true) where
  total := fun a b => by simpa using total a b
Decidable Total Relation Preserves Totality
Informal description
For any type $\alpha$ with a decidable total relation $r$, the relation defined by $(a, b) \mapsto \text{decide}(r(a, b)) = \text{true}$ is also total.
IsTrichotomous.decide instance
[DecidableRel r] [IsTrichotomous α r] : IsTrichotomous α (fun a b => decide (r a b) = true)
Full source 
instance IsTrichotomous.decide [DecidableRel r] [IsTrichotomous α r] :
    IsTrichotomous α (fun a b => decide (r a b) = true) where
  trichotomous := fun a b => by simpa using trichotomous a b
Decidable Trichotomous Relation Preserves Trichotomy
Informal description
For any type $\alpha$ with a decidable trichotomous relation $r$, the relation defined by $(a, b) \mapsto \text{decide}(r(a, b)) = \text{true}$ is also trichotomous.
irrefl_of theorem
[IsIrrefl α r] (a : α) : ¬a ≺ a
Full source 
@[elab_without_expected_type] lemma irrefl_of [IsIrrefl α r] (a : α) : ¬a ≺ a := irrefl a
Irreflexivity Property of a Binary Relation
Informal description
For any irreflexive binary relation $\prec$ on a type $\alpha$ and any element $a \in \alpha$, the relation $a \prec a$ does not hold.
refl_of theorem
[IsRefl α r] (a : α) : a ≺ a
Full source 
@[elab_without_expected_type] lemma refl_of [IsRefl α r] (a : α) : a ≺ a := refl a
Reflexivity of a Binary Relation
Informal description
For any reflexive binary relation $\prec$ on a type $\alpha$ and any element $a \in \alpha$, we have $a \prec a$.
trans_of theorem
[IsTrans α r] : a ≺ b → b ≺ c → a ≺ c
Full source 
@[elab_without_expected_type] lemma trans_of [IsTrans α r] : a ≺ b → b ≺ c → a ≺ c := _root_.trans
Transitivity of Binary Relations: $a \prec b \land b \prec c \implies a \prec c$
Informal description
For any transitive binary relation $\prec$ on a type $\alpha$ and any elements $a, b, c \in \alpha$, if $a \prec b$ and $b \prec c$ hold, then $a \prec c$ also holds.
symm_of theorem
[IsSymm α r] : a ≺ b → b ≺ a
Full source 
@[elab_without_expected_type] lemma symm_of [IsSymm α r] : a ≺ b → b ≺ a := symm
Symmetry Property: $a \prec b \implies b \prec a$
Informal description
For any symmetric binary relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a \prec b$ holds, then $b \prec a$ also holds.
asymm_of theorem
[IsAsymm α r] : a ≺ b → ¬b ≺ a
Full source 
@[elab_without_expected_type] lemma asymm_of [IsAsymm α r] : a ≺ b → ¬b ≺ a := asymm
Asymmetry Property: $a \prec b \implies \neg(b \prec a)$
Informal description
For any asymmetric binary relation $\prec$ on a type $\alpha$, if $a \prec b$ holds for some elements $a, b \in \alpha$, then $b \prec a$ does not hold.
total_of theorem
[IsTotal α r] (a b : α) : a ≺ b ∨ b ≺ a
Full source 
@[elab_without_expected_type]
lemma total_of [IsTotal α r] (a b : α) : a ≺ b ∨ b ≺ a := IsTotal.total _ _
Totality of a Binary Relation
Informal description
For any binary relation $r$ on a type $\alpha$ that is total, and for any two elements $a$ and $b$ in $\alpha$, either $a \prec b$ or $b \prec a$ holds.
trichotomous_of theorem
[IsTrichotomous α r] : ∀ a b : α, a ≺ b ∨ a = b ∨ b ≺ a
Full source 
@[elab_without_expected_type]
lemma trichotomous_of [IsTrichotomous α r] : ∀ a b : α, a ≺ b ∨ a = b ∨ b ≺ a := trichotomous
Trichotomy Property for Trichotomous Relations
Informal description
For any type $\alpha$ with a trichotomous relation $\prec$, and for any elements $a, b \in \alpha$, exactly one of the following holds: $a \prec b$, $a = b$, or $b \prec a$.
Reflexive definition
Full source 
/-- `IsRefl` as a definition, suitable for use in proofs. -/
def Reflexive := ∀ x, x ≺ x
Reflexive relation
Informal description
A binary relation $\prec$ on a type is called *reflexive* if for every element $x$, the relation $x \prec x$ holds.
Symmetric definition
Full source 
/-- `IsSymm` as a definition, suitable for use in proofs. -/
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
Symmetric relation
Informal description
A binary relation $\prec$ on a type is called *symmetric* if for all elements $x$ and $y$, whenever $x \prec y$ holds, then $y \prec x$ also holds.
Transitive definition
Full source 
/-- `IsTrans` as a definition, suitable for use in proofs. -/
def Transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
Transitive relation
Informal description
A binary relation $\prec$ on a type is called *transitive* if for all elements $x$, $y$, and $z$, whenever $x \prec y$ and $y \prec z$ hold, then $x \prec z$ also holds.
Irreflexive definition
Full source 
/-- `IsIrrefl` as a definition, suitable for use in proofs. -/
def Irreflexive := ∀ x, ¬x ≺ x
Irreflexive relation
Informal description
A binary relation $\prec$ on a type is called *irreflexive* if for every element $x$, it is not the case that $x \prec x$.
AntiSymmetric definition
Full source 
/-- `IsAntisymm` as a definition, suitable for use in proofs. -/
def AntiSymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y
Antisymmetric relation
Informal description
A binary relation $\prec$ on a type is called *antisymmetric* if for all elements $x$ and $y$, whenever $x \prec y$ and $y \prec x$ hold, then $x = y$.
Total definition
Full source 
/-- `IsTotal` as a definition, suitable for use in proofs. -/
def Total := ∀ x y, x ≺ y ∨ y ≺ x
Total relation
Informal description
A binary relation $\prec$ on a type is called *total* if for any two elements $x$ and $y$, either $x \prec y$ or $y \prec x$ holds.
Equivalence.reflexive theorem
(h : Equivalence r) : Reflexive r
Full source 
theorem Equivalence.reflexive (h : Equivalence r) : Reflexive r := h.refl
Reflexivity of Equivalence Relations
Informal description
For any equivalence relation $r$, the relation $r$ is reflexive. That is, for every element $x$, the relation $x \mathbin{r} x$ holds.
Equivalence.symmetric theorem
(h : Equivalence r) : Symmetric r
Full source 
theorem Equivalence.symmetric (h : Equivalence r) : Symmetric r :=
  fun _ _ ↦ h.symm
Symmetry of Equivalence Relations
Informal description
For any equivalence relation $r$, the relation $r$ is symmetric. That is, if $x \mathbin{r} y$ holds, then $y \mathbin{r} x$ also holds.
Equivalence.transitive theorem
(h : Equivalence r) : Transitive r
Full source 
theorem Equivalence.transitive (h : Equivalence r) : Transitive r :=
  fun _ _ _ ↦ h.trans
Transitivity of Equivalence Relations
Informal description
For any equivalence relation $r$, the relation $r$ is transitive. That is, if $x \mathbin{r} y$ and $y \mathbin{r} z$ hold, then $x \mathbin{r} z$ also holds.
InvImage.trans theorem
(h : Transitive r) : Transitive (InvImage r f)
Full source 
theorem InvImage.trans (h : Transitive r) : Transitive (InvImage r f) :=
  fun (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃) ↦ h h₁ h₂
Transitivity Preservation under Inverse Image Relation
Informal description
Given a transitive relation $r$ on a type and a function $f$ mapping elements of another type to this type, the relation defined by $x \prec y$ if and only if $f(x) \prec f(y)$ under $r$ is also transitive.
InvImage.irreflexive theorem
(h : Irreflexive r) : Irreflexive (InvImage r f)
Full source 
theorem InvImage.irreflexive (h : Irreflexive r) : Irreflexive (InvImage r f) :=
  fun (a : α) (h₁ : InvImage r f a a) ↦ h (f a) h₁
Irreflexivity Preservation under Inverse Image Relation
Informal description
Given a binary relation $r$ on a type $\beta$ that is irreflexive, and a function $f : \alpha \to \beta$, the relation $\text{InvImage}\, r\, f$ on $\alpha$ defined by $x \prec y \leftrightarrow f(x) \prec f(y)$ is also irreflexive.
Minimal definition
(P : α → Prop) (x : α) : Prop
Full source 
/-- `Minimal P x` means that `x` is a minimal element satisfying `P`. -/
def Minimal (P : α → Prop) (x : α) : Prop := P x ∧ ∀ ⦃y⦄, P y → y ≤ x → x ≤ y
Minimal element with respect to a predicate
Informal description
Given a predicate \( P \) on a type \( \alpha \) with a preorder, an element \( x \) is called *minimal* with respect to \( P \) if \( P(x) \) holds and for any \( y \) satisfying \( P(y) \), if \( y \leq x \) then \( x \leq y \).
Maximal definition
(P : α → Prop) (x : α) : Prop
Full source 
/-- `Maximal P x` means that `x` is a maximal element satisfying `P`. -/
def Maximal (P : α → Prop) (x : α) : Prop := P x ∧ ∀ ⦃y⦄, P y → x ≤ y → y ≤ x
Maximal element with respect to a predicate
Informal description
Given a preorder on a type $\alpha$ and a predicate $P$ on $\alpha$, an element $x$ is called *maximal* with respect to $P$ if $P(x)$ holds and for any $y$ satisfying $P(y)$, if $x \leq y$ then $y \leq x$.
Minimal.prop theorem
(h : Minimal P x) : P x
Full source 
lemma Minimal.prop (h : Minimal P x) : P x :=
  h.1
Minimal elements satisfy their predicate
Informal description
If an element $x$ is minimal with respect to a predicate $P$ on a preordered type $\alpha$, then $P(x)$ holds.
Maximal.prop theorem
(h : Maximal P x) : P x
Full source 
lemma Maximal.prop (h : Maximal P x) : P x :=
  h.1
Maximal elements satisfy their predicate
Informal description
If an element $x$ is maximal with respect to a predicate $P$ in a preorder, then $P(x)$ holds.
Minimal.le_of_le theorem
(h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y
Full source 
lemma Minimal.le_of_le (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y :=
  h.2 hy hle
Minimal Element Property: $y \leq x$ implies $x \leq y$ for minimal elements
Informal description
Let $P$ be a predicate on a preordered type $\alpha$, and let $x \in \alpha$ be a minimal element with respect to $P$. For any $y \in \alpha$ satisfying $P(y)$, if $y \leq x$, then $x \leq y$.
Maximal.le_of_ge theorem
(h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x
Full source 
lemma Maximal.le_of_ge (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x :=
  h.2 hy hge
Maximal Element Property: $x \leq y$ implies $y \leq x$ for maximal elements
Informal description
Let $P$ be a predicate on a preordered type $\alpha$, and let $x \in \alpha$ be a maximal element with respect to $P$. For any $y \in \alpha$ satisfying $P(y)$, if $x \leq y$, then $y \leq x$.
MinimalFor definition
(P : ι → Prop) (f : ι → α) (i : ι) : Prop
Full source 
/-- `Minimal P i` means that `i` is an element with minimal image along `f` satisfying `P`. -/
def MinimalFor (P : ι → Prop) (f : ι → α) (i : ι) : Prop := P i ∧ ∀ ⦃j⦄, P j → f j ≤ f i → f i ≤ f j
Minimal element with respect to a function
Informal description
Given a predicate \( P \) on a type \( \iota \) and a function \( f : \iota \to \alpha \) where \( \alpha \) is a preorder, an element \( i \in \iota \) is called *minimal for \( P \) with respect to \( f \)* if: 1. \( P(i) \) holds, and 2. For any \( j \in \iota \) such that \( P(j) \) holds and \( f(j) \leq f(i) \), we have \( f(i) \leq f(j) \). In other words, \( i \) is minimal if it satisfies \( P \) and any other element \( j \) satisfying \( P \) with \( f(j) \) not greater than \( f(i) \) must have \( f(j) \) equal to \( f(i) \).
MaximalFor definition
(P : ι → Prop) (f : ι → α) (i : ι) : Prop
Full source 
/-- `Maximal P i` means that `i` is an element with minimal image along `f` satisfying `P`. -/
def MaximalFor (P : ι → Prop) (f : ι → α) (i : ι) : Prop := P i ∧ ∀ ⦃j⦄, P j → f i ≤ f j → f j ≤ f i
Maximal element with respect to a function and predicate
Informal description
Given a predicate \( P \) on a type \( \iota \) and a function \( f : \iota \to \alpha \) where \( \alpha \) is an ordered type, an element \( i \in \iota \) is called *maximal for \( P \) with respect to \( f \)* if: 1. \( P(i) \) holds, and 2. For any \( j \in \iota \) such that \( P(j) \) holds and \( f(i) \leq f(j) \), we have \( f(j) \leq f(i) \). In other words, \( i \) is maximal if it satisfies \( P \) and any other element \( j \) satisfying \( P \) with \( f(i) \leq f(j) \) must have \( f(j) \leq f(i) \).
MinimalFor.prop theorem
(h : MinimalFor P f i) : P i
Full source 
lemma MinimalFor.prop (h : MinimalFor P f i) : P i := h.1
Minimal Elements Satisfy the Predicate
Informal description
If an element $i$ is minimal for a predicate $P$ with respect to a function $f$, then $P(i)$ holds.
MaximalFor.prop theorem
(h : MaximalFor P f i) : P i
Full source 
lemma MaximalFor.prop (h : MaximalFor P f i) : P i := h.1
Maximality Implies Predicate Satisfaction
Informal description
If $i$ is a maximal element for the predicate $P$ with respect to the function $f$, then $P(i)$ holds.
MinimalFor.le_of_le theorem
(h : MinimalFor P f i) (hj : P j) (hji : f j ≤ f i) : f i ≤ f j
Full source 
lemma MinimalFor.le_of_le (h : MinimalFor P f i) (hj : P j) (hji : f j ≤ f i) : f i ≤ f j :=
  h.2 hj hji
Minimality implies symmetric inequality for comparable elements
Informal description
Let $P$ be a predicate on a type $\iota$, $f : \iota \to \alpha$ a function where $\alpha$ is a preorder, and $i \in \iota$ a minimal element for $P$ with respect to $f$. For any $j \in \iota$ satisfying $P(j)$ with $f(j) \leq f(i)$, we have $f(i) \leq f(j)$.
MaximalFor.le_of_le theorem
(h : MaximalFor P f i) (hj : P j) (hij : f i ≤ f j) : f j ≤ f i
Full source 
lemma MaximalFor.le_of_le (h : MaximalFor P f i) (hj : P j) (hij : f i ≤ f j) : f j ≤ f i :=
  h.2 hj hij
Maximality implies reverse inequality for comparable elements
Informal description
Let $P$ be a predicate on a type $\iota$, $f : \iota \to \alpha$ a function where $\alpha$ is an ordered type, and $i \in \iota$ a maximal element for $P$ with respect to $f$. For any $j \in \iota$ satisfying $P(j)$ with $f(i) \leq f(j)$, we have $f(j) \leq f(i)$.
IsUpperSet definition
{α : Type*} [LE α] (s : Set α) : Prop
Full source 
/-- An upper set in an order `α` is a set such that any element greater than one of its members is
also a member. Also called up-set, upward-closed set. -/
def IsUpperSet {α : Type*} [LE α] (s : Set α) : Prop :=
  ∀ ⦃a b : α⦄, a ≤ b → a ∈ s → b ∈ s
Upper set
Informal description
A subset $s$ of a type $\alpha$ with a preorder relation $\leq$ is called an *upper set* if for any elements $a, b \in \alpha$, whenever $a \leq b$ and $a \in s$, then $b \in s$. In other words, an upper set is closed under taking elements greater than any of its members.
IsLowerSet definition
{α : Type*} [LE α] (s : Set α) : Prop
Full source 
/-- A lower set in an order `α` is a set such that any element less than one of its members is also
a member. Also called down-set, downward-closed set. -/
def IsLowerSet {α : Type*} [LE α] (s : Set α) : Prop :=
  ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s
Lower set (down-set)
Informal description
A subset $s$ of a type $\alpha$ with a preorder relation $\leq$ is called a *lower set* if for any elements $a, b \in \alpha$, whenever $b \leq a$ and $a \in s$, then $b \in s$. In other words, a lower set is closed under taking elements less than any of its members. Lower sets are also called down-sets or downward-closed sets.
UpperSet structure
(α : Type*) [LE α]
Full source 
@[inherit_doc IsUpperSet]
structure UpperSet (α : Type*) [LE α] where
  /-- The carrier of an `UpperSet`. -/
  carrier : Set α
  /-- The carrier of an `UpperSet` is an upper set. -/
  upper' : IsUpperSet carrier
Upper set in a preorder
Informal description
An upper set in a type $\alpha$ equipped with a preorder relation $\leq$ is a subset $S \subseteq \alpha$ such that for any $x \in S$ and $y \in \alpha$, if $x \leq y$ then $y \in S$. In other words, it is a set that is closed under taking elements greater than any of its members.
LowerSet structure
(α : Type*) [LE α]
Full source 
@[inherit_doc IsLowerSet]
structure LowerSet (α : Type*) [LE α] where
  /-- The carrier of a `LowerSet`. -/
  carrier : Set α
  /-- The carrier of a `LowerSet` is a lower set. -/
  lower' : IsLowerSet carrier
Lower set in a preorder
Informal description
A lower set in a type $\alpha$ equipped with a preorder (reflexive and transitive relation) is a subset $S \subseteq \alpha$ such that for any $x \in S$ and $y \leq x$, we have $y \in S$.
of_eq theorem
[IsRefl α r] : ∀ {a b}, a = b → r a b
Full source 
theorem of_eq [IsRefl α r] : ∀ {a b}, a = b → r a b
  | _, _, .refl _ => refl _
Reflexive Relation Preserves Equality: $a = b \Rightarrow a \prec b$
Informal description
For any reflexive binary relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a = b$ then $a \prec b$.
comm theorem
[IsSymm α r] {a b : α} : r a b ↔ r b a
Full source 
theorem comm [IsSymm α r] {a b : α} : r a b ↔ r b a :=
  ⟨symm, symm⟩
Symmetry of Binary Relation: $a \prec b \leftrightarrow b \prec a$
Informal description
For any symmetric binary relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, the relation $a \prec b$ holds if and only if $b \prec a$ holds.
antisymm' theorem
[IsAntisymm α r] {a b : α} : r a b → r b a → b = a
Full source 
theorem antisymm' [IsAntisymm α r] {a b : α} : r a b → r b a → b = a := fun h h' => antisymm h' h
Antisymmetry of Relation: $a \prec b \land b \prec a \Rightarrow b = a$
Informal description
For any antisymmetric relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a \prec b$ and $b \prec a$ hold, then $b = a$.
antisymm_iff theorem
[IsRefl α r] [IsAntisymm α r] {a b : α} : r a b ∧ r b a ↔ a = b
Full source 
theorem antisymm_iff [IsRefl α r] [IsAntisymm α r] {a b : α} : r a b ∧ r b ar a b ∧ r b a ↔ a = b :=
  ⟨fun h => antisymm h.1 h.2, by
    rintro rfl
    exact ⟨refl _, refl _⟩⟩
Characterization of Equality via Reflexive and Antisymmetric Relation: $a \prec b \land b \prec a \leftrightarrow a = b$
Informal description
For any reflexive and antisymmetric binary relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, the relation $a \prec b$ and $b \prec a$ holds if and only if $a = b$.
antisymm_of theorem
(r : α → α → Prop) [IsAntisymm α r] {a b : α} : r a b → r b a → a = b
Full source 
/-- A version of `antisymm` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there. -/
@[elab_without_expected_type]
theorem antisymm_of (r : α → α → Prop) [IsAntisymm α r] {a b : α} : r a b → r b a → a = b :=
  antisymm
Antisymmetry of Relation: $a \prec b \land b \prec a \Rightarrow a = b$
Informal description
For any antisymmetric relation $\prec$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a \prec b$ and $b \prec a$ hold, then $a = b$.
antisymm_of' theorem
(r : α → α → Prop) [IsAntisymm α r] {a b : α} : r a b → r b a → b = a
Full source 
/-- A version of `antisymm'` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there. -/
@[elab_without_expected_type]
theorem antisymm_of' (r : α → α → Prop) [IsAntisymm α r] {a b : α} : r a b → r b a → b = a :=
  antisymm'
Antisymmetry of Relation: $r(a, b) \land r(b, a) \Rightarrow b = a$
Informal description
For any antisymmetric relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $r(a, b)$ and $r(b, a)$ hold, then $b = a$.
comm_of theorem
(r : α → α → Prop) [IsSymm α r] {a b : α} : r a b ↔ r b a
Full source 
/-- A version of `comm` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there. -/
theorem comm_of (r : α → α → Prop) [IsSymm α r] {a b : α} : r a b ↔ r b a :=
  comm
Symmetry of Relation: $r(a, b) \leftrightarrow r(b, a)$
Informal description
For any symmetric binary relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, the relation $r(a, b)$ holds if and only if $r(b, a)$ holds.
IsAsymm.isIrrefl theorem
[IsAsymm α r] : IsIrrefl α r
Full source 
protected theorem IsAsymm.isIrrefl [IsAsymm α r] : IsIrrefl α r :=
  ⟨fun _ h => _root_.asymm h h⟩
Asymmetry Implies Irreflexivity for Binary Relations
Informal description
For any binary relation $\prec$ on a type $\alpha$, if $\prec$ is asymmetric, then it is also irreflexive. That is, for any $a \in \alpha$, $a \prec a$ does not hold.
IsTotal.isTrichotomous theorem
(r) [IsTotal α r] : IsTrichotomous α r
Full source 
protected theorem IsTotal.isTrichotomous (r) [IsTotal α r] : IsTrichotomous α r :=
  ⟨fun a b => or_left_comm.1 (Or.inr <| total_of r a b)⟩
Total Relation Implies Trichotomy
Informal description
For any binary relation $r$ on a type $\alpha$, if $r$ is total (i.e., for any $a, b \in \alpha$, either $a \prec b$ or $b \prec a$ holds), then $r$ is trichotomous (i.e., for any $a, b \in \alpha$, exactly one of $a \prec b$, $a = b$, or $b \prec a$ holds).
ne_of_irrefl theorem
{r} [IsIrrefl α r] : ∀ {x y : α}, r x y → x ≠ y
Full source 
theorem ne_of_irrefl {r} [IsIrrefl α r] : ∀ {x y : α}, r x y → x ≠ y
  | _, _, h, rfl => irrefl _ h
Irreflexive Relation Implies Inequality
Informal description
For any irreflexive binary relation $\prec$ on a type $\alpha$ and any elements $x, y \in \alpha$, if $x \prec y$ holds, then $x \neq y$.
ne_of_irrefl' theorem
{r} [IsIrrefl α r] : ∀ {x y : α}, r x y → y ≠ x
Full source 
theorem ne_of_irrefl' {r} [IsIrrefl α r] : ∀ {x y : α}, r x y → y ≠ x
  | _, _, h, rfl => irrefl _ h
Irreflexive Relation Implies Inequality in Reverse Order
Informal description
For any irreflexive binary relation $\prec$ on a type $\alpha$ and any elements $x, y \in \alpha$, if $x \prec y$ holds, then $y \neq x$.
not_rel_of_subsingleton theorem
(r) [IsIrrefl α r] [Subsingleton α] (x y) : ¬r x y
Full source 
theorem not_rel_of_subsingleton (r) [IsIrrefl α r] [Subsingleton α] (x y) : ¬r x y :=
  Subsingleton.elim x y ▸ irrefl x
Irreflexive Relation on Subsingleton is Empty
Informal description
For any irreflexive binary relation $\prec$ on a type $\alpha$ that is a subsingleton (i.e., has at most one distinct element), and for any elements $x, y \in \alpha$, the relation $x \prec y$ does not hold.
rel_of_subsingleton theorem
(r) [IsRefl α r] [Subsingleton α] (x y) : r x y
Full source 
theorem rel_of_subsingleton (r) [IsRefl α r] [Subsingleton α] (x y) : r x y :=
  Subsingleton.elim x y ▸ refl x
Reflexive Relation on Subsingleton is Total
Informal description
For any reflexive binary relation $\prec$ on a type $\alpha$ that is a subsingleton (i.e., has at most one distinct element), and for any elements $x, y \in \alpha$, the relation $x \prec y$ holds.
empty_relation_apply theorem
(a b : α) : EmptyRelation a b ↔ False
Full source 
@[simp]
theorem empty_relation_apply (a b : α) : EmptyRelationEmptyRelation a b ↔ False :=
  Iff.rfl
Empty Relation is Always False
Informal description
For any elements $a$ and $b$ of type $\alpha$, the empty relation $\text{EmptyRelation}(a, b)$ holds if and only if $\text{False}$.
instIsIrreflEmptyRelation instance
: IsIrrefl α EmptyRelation
Full source 
instance : IsIrrefl α EmptyRelation :=
  ⟨fun _ => id⟩
Irreflexivity of the Empty Relation
Informal description
The empty relation on any type $\alpha$ is irreflexive, meaning that for any element $x \in \alpha$, the relation $\text{EmptyRelation}(x, x)$ does not hold.
rel_congr_left theorem
[IsSymm α r] [IsTrans α r] {a b c : α} (h : r a b) : r a c ↔ r b c
Full source 
theorem rel_congr_left [IsSymm α r] [IsTrans α r] {a b c : α} (h : r a b) : r a c ↔ r b c :=
  ⟨trans_of r (symm_of r h), trans_of r h⟩
Congruence of Relation on Left Argument: $a \prec b \implies (a \prec c \leftrightarrow b \prec c)$
Informal description
For a symmetric and transitive relation $\prec$ on a type $\alpha$ and elements $a, b, c \in \alpha$, if $a \prec b$ holds, then $a \prec c$ if and only if $b \prec c$.
rel_congr_right theorem
[IsSymm α r] [IsTrans α r] {a b c : α} (h : r b c) : r a b ↔ r a c
Full source 
theorem rel_congr_right [IsSymm α r] [IsTrans α r] {a b c : α} (h : r b c) : r a b ↔ r a c :=
  ⟨(trans_of r · h), (trans_of r · (symm_of r h))⟩
Congruence of Relation on Right Argument: $b \prec c \implies (a \prec b \leftrightarrow a \prec c)$
Informal description
For a symmetric and transitive relation $\prec$ on a type $\alpha$ and elements $a, b, c \in \alpha$, if $b \prec c$ holds, then $a \prec b$ if and only if $a \prec c$.
rel_congr theorem
[IsSymm α r] [IsTrans α r] {a b c d : α} (h₁ : r a b) (h₂ : r c d) : r a c ↔ r b d
Full source 
theorem rel_congr [IsSymm α r] [IsTrans α r] {a b c d : α} (h₁ : r a b) (h₂ : r c d) :
    r a c ↔ r b d := by
  rw [rel_congr_left h₁, rel_congr_right h₂]
Congruence of Relation: $a \prec b \land c \prec d \implies (a \prec c \leftrightarrow b \prec d)$
Informal description
For a symmetric and transitive relation $\prec$ on a type $\alpha$ and elements $a, b, c, d \in \alpha$, if $a \prec b$ and $c \prec d$ hold, then $a \prec c$ if and only if $b \prec d$.
trans_trichotomous_left theorem
[IsTrans α r] [IsTrichotomous α r] {a b c : α} (h₁ : ¬r b a) (h₂ : r b c) : r a c
Full source 
theorem trans_trichotomous_left [IsTrans α r] [IsTrichotomous α r] {a b c : α}
    (h₁ : ¬r b a) (h₂ : r b c) : r a c := by
  rcases trichotomous_of r a b with (h₃ | rfl | h₃)
  · exact _root_.trans h₃ h₂
  · exact h₂
  · exact absurd h₃ h₁
Transitivity from Trichotomy on Left: $b \not\prec a \land b \prec c \implies a \prec c$
Informal description
Let $\prec$ be a transitive and trichotomous relation on a type $\alpha$. For any elements $a, b, c \in \alpha$, if $b \not\prec a$ and $b \prec c$ hold, then $a \prec c$.
trans_trichotomous_right theorem
[IsTrans α r] [IsTrichotomous α r] {a b c : α} (h₁ : r a b) (h₂ : ¬r c b) : r a c
Full source 
theorem trans_trichotomous_right [IsTrans α r] [IsTrichotomous α r] {a b c : α}
    (h₁ : r a b) (h₂ : ¬r c b) : r a c := by
  rcases trichotomous_of r b c with (h₃ | rfl | h₃)
  · exact _root_.trans h₁ h₃
  · exact h₁
  · exact absurd h₃ h₂
Transitivity and Trichotomy Imply Right Transitivity: $a \prec b \land \neg(c \prec b) \implies a \prec c$
Informal description
Let $\prec$ be a transitive and trichotomous relation on a type $\alpha$. For any elements $a, b, c \in \alpha$, if $a \prec b$ and it is not the case that $c \prec b$, then $a \prec c$.
transitive_of_trans theorem
(r : α → α → Prop) [IsTrans α r] : Transitive r
Full source 
theorem transitive_of_trans (r : α → α → Prop) [IsTrans α r] : Transitive r := IsTrans.trans
Transitivity Implies `Transitive` Property
Informal description
For any binary relation $r$ on a type $\alpha$, if $r$ is transitive (i.e., for all $x, y, z \in \alpha$, $r(x, y)$ and $r(y, z)$ imply $r(x, z)$), then $r$ satisfies the `Transitive` property.
extensional_of_trichotomous_of_irrefl theorem
(r : α → α → Prop) [IsTrichotomous α r] [IsIrrefl α r] {a b : α} (H : ∀ x, r x a ↔ r x b) : a = b
Full source 
/-- In a trichotomous irreflexive order, every element is determined by the set of predecessors. -/
theorem extensional_of_trichotomous_of_irrefl (r : α → α → Prop) [IsTrichotomous α r] [IsIrrefl α r]
    {a b : α} (H : ∀ x, r x a ↔ r x b) : a = b :=
  ((@trichotomous _ r _ a b).resolve_left <| mt (H _).2 <| irrefl a).resolve_right <| mt (H _).1
    <| irrefl b
Extensionality in Trichotomous Irreflexive Orders
Informal description
Let $\prec$ be a binary relation on a type $\alpha$ that is trichotomous and irreflexive. If for every element $x \in \alpha$, the relations $x \prec a$ and $x \prec b$ are equivalent, then $a = b$.