# Documentation

Mathlib.Order.RelClasses

# Unbundled relation classes #

In this file we prove some properties of Is* classes defined in Init.Algebra.Classes. The main difference between these classes and the usual order classes (Preorder etc) is that usual classes extend LE and/or LT while these classes take a relation as an explicit argument.

theorem of_eq {α : Type u} {r : ααProp} [inst : IsRefl α r] {a : α} {b : α} :
a = br a b
theorem comm {α : Type u} {r : ααProp} [inst : IsSymm α r] {a : α} {b : α} :
r a b r b a
theorem antisymm' {α : Type u} {r : ααProp} [inst : ] {a : α} {b : α} :
r a br b ab = a
theorem antisymm_iff {α : Type u} {r : ααProp} [inst : IsRefl α r] [inst : ] {a : α} {b : α} :
r a b r b a a = b
@[elab_without_expected_type]
theorem antisymm_of {α : Type u} (r : ααProp) [inst : ] {a : α} {b : α} :
r a br b aa = b

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' {α : Type u} (r : ααProp) [inst : ] {a : α} {b : α} :
r a br b ab = a

A version of antisymm' with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

theorem comm_of {α : Type u} (r : ααProp) [inst : IsSymm α r] {a : α} {b : α} :
r a b r b a

A version of comm with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

theorem IsRefl.swap {α : Type u} (r : ααProp) [inst : IsRefl α r] :
IsRefl α ()
theorem IsIrrefl.swap {α : Type u} (r : ααProp) [inst : IsIrrefl α r] :
theorem IsTrans.swap {α : Type u} (r : ααProp) [inst : IsTrans α r] :
IsTrans α ()
theorem IsAntisymm.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsAsymm.swap {α : Type u} (r : ααProp) [inst : IsAsymm α r] :
IsAsymm α ()
theorem IsTotal.swap {α : Type u} (r : ααProp) [inst : IsTotal α r] :
IsTotal α ()
theorem IsTrichotomous.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsPreorder.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsStrictOrder.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsPartialOrder.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsTotalPreorder.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsLinearOrder.swap {α : Type u} (r : ααProp) [inst : ] :
theorem IsAsymm.isAntisymm {α : Type u} (r : ααProp) [inst : IsAsymm α r] :
theorem IsAsymm.isIrrefl {α : Type u} {r : ααProp} [inst : IsAsymm α r] :
theorem IsTotal.isTrichotomous {α : Type u} (r : ααProp) [inst : IsTotal α r] :
instance IsTotal.to_isRefl {α : Type u} (r : ααProp) [inst : IsTotal α r] :
IsRefl α r
Equations
theorem ne_of_irrefl {α : Type u} {r : ααProp} [inst : IsIrrefl α r] {x : α} {y : α} :
r x yx y
theorem ne_of_irrefl' {α : Type u} {r : ααProp} [inst : IsIrrefl α r] {x : α} {y : α} :
r x yy x
theorem not_rel_of_subsingleton {α : Type u} (r : ααProp) [inst : IsIrrefl α r] [inst : ] (x : α) (y : α) :
¬r x y
theorem rel_of_subsingleton {α : Type u} (r : ααProp) [inst : IsRefl α r] [inst : ] (x : α) (y : α) :
r x y
@[simp]
theorem empty_relation_apply {α : Type u} (a : α) (b : α) :
theorem eq_empty_relation {α : Type u} (r : ααProp) [inst : IsIrrefl α r] [inst : ] :
r = EmptyRelation
instance instIsIrreflEmptyRelation {α : Type u} :
IsIrrefl α EmptyRelation
Equations
theorem trans_trichotomous_left {α : Type u} {r : ααProp} [inst : IsTrans α r] [inst : ] {a : α} {b : α} {c : α} :
¬r b ar b cr a c
theorem trans_trichotomous_right {α : Type u} {r : ααProp} [inst : IsTrans α r] [inst : ] {a : α} {b : α} {c : α} :
r a b¬r c br a c
theorem transitive_of_trans {α : Type u} (r : ααProp) [inst : IsTrans α r] :
theorem extensional_of_trichotomous_of_irrefl {α : Type u} (r : ααProp) [inst : ] [inst : IsIrrefl α r] {a : α} {b : α} (H : ∀ (x : α), r x a r x b) :
a = b

In a trichotomous irreflexive order, every element is determined by the set of predecessors.

def partialOrderOfSO {α : Type u} (r : ααProp) [inst : ] :

Construct a partial order from a isStrictOrder relation.

See note [reducible non-instances].

Equations
def linearOrderOfSTO {α : Type u} (r : ααProp) [inst : ] [inst : (x y : α) → Decidable ¬r x y] :

Construct a linear order from an IsStrictTotalOrder relation.

See note [reducible non-instances].

Equations
• One or more equations did not get rendered due to their size.
theorem IsStrictTotalOrder.swap {α : Type u} (r : ααProp) [inst : ] :

### Order connection #

class IsOrderConnected (α : Type u) (lt : ααProp) :
• A connected order is one satisfying the condition a < c → a < b ∨ b < c→ a < b ∨ b < c∨ b < c.

conn : ∀ (a b c : α), lt a clt a b lt b c

A connected order is one satisfying the condition a < c → a < b ∨ b < c→ a < b ∨ b < c∨ b < c. This is recognizable as an intuitionistic substitute for a ≤ b ∨ b ≤ a≤ b ∨ b ≤ a∨ b ≤ a≤ a on the constructive reals, and is also known as negative transitivity, since the contrapositive asserts transitivity of the relation ¬ a < b¬ a < b.

Instances
theorem IsOrderConnected.neg_trans {α : Type u} {r : ααProp} [inst : ] {a : α} {b : α} {c : α} (h₁ : ¬r a b) (h₂ : ¬r b c) :
¬r a c
theorem isStrictWeakOrder_of_isOrderConnected {α : Type u} {r : ααProp} [inst : IsAsymm α r] [inst : ] :
instance isStrictOrderConnected_of_isStrictTotalOrder {α : Type u} {r : ααProp} [inst : ] :
Equations
instance isStrictTotalOrder_of_isStrictTotalOrder {α : Type u} {r : ααProp} [inst : ] :
Equations

### Well-order #

theorem IsWellFounded_iff (α : Type u) (r : ααProp) :
class IsWellFounded (α : Type u) (r : ααProp) :
• The relation is WellFounded, as a proposition.

wf :

A well-founded relation. Not to be confused with isWellOrder.

Instances
instance instIsWellFoundedRel {α : Type u} [h : ] :
IsWellFounded α WellFoundedRelation.rel
Equations
theorem WellFoundedRelation.asymmetric {α : Sort u_1} [inst : ] {a : α} {b : α} :
theorem WellFounded.prod_lex {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} (ha : ) (hb : ) :
theorem IsWellFounded.induction {α : Type u} (r : ααProp) [inst : ] {C : αProp} (a : α) :
((x : α) → ((y : α) → r y xC y) → C x) → C a

Induction on a well-founded relation.

theorem IsWellFounded.apply {α : Type u} (r : ααProp) [inst : ] (a : α) :
Acc r a

All values are accessible under the well-founded relation.

noncomputable def IsWellFounded.fix {α : Type u} (r : ααProp) [inst : ] {C : αSort u_1} :
((x : α) → ((y : α) → r y xC y) → C x) → (x : α) → C x

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.

Equations
theorem IsWellFounded.fix_eq {α : Type u} (r : ααProp) [inst : ] {C : αSort u_1} (F : (x : α) → ((y : α) → r y xC y) → C x) (x : α) :
= F x fun y x =>

The value from IsWellFounded.fix is built from the previous ones as specified.

def IsWellFounded.toWellFoundedRelation {α : Type u} (r : ααProp) [inst : ] :

Derive a WellFoundedRelation instance from an isWellFounded instance.

Equations
• = { rel := r, wf := (_ : ) }
theorem WellFounded.asymmetric {α : Sort u_1} {r : ααProp} (h : ) (a : α) (b : α) :
r a b¬r b a
instance instIsAsymm {α : Type u} (r : ααProp) [inst : ] :
IsAsymm α r
Equations
instance instIsIrrefl {α : Type u} (r : ααProp) [inst : ] :
Equations
def WellFoundedLT (α : Type u_1) [inst : LT α] :

A class for a well founded relation <.

Equations
def WellFoundedGT (α : Type u_1) [inst : LT α] :

A class for a well founded relation >.

Equations
instance instWellFoundedGTOrderDualInstLTOrderDual (α : Type u_1) [inst : LT α] [h : ] :
Equations
instance instWellFoundedLTOrderDualInstLTOrderDual (α : Type u_1) [inst : LT α] [h : ] :
Equations
theorem wellFoundedGT_dual_iff (α : Type u_1) [inst : LT α] :
theorem wellFoundedLT_dual_iff (α : Type u_1) [inst : LT α] :
class IsWellOrder (α : Type u) (r : ααProp) extends , , :

A well order is a well-founded linear order.

Instances
instance instIsStrictTotalOrder {α : Type u_1} (r : ααProp) [inst : ] :
Equations
instance instIsTrichotomous {α : Type u_1} (r : ααProp) [inst : ] :
Equations
instance instIsTrans_1 {α : Type u_1} (r : ααProp) [inst : ] :
IsTrans α r
Equations
instance instIsIrrefl_1 {α : Type u_1} (r : ααProp) [inst : ] :
Equations
instance instIsAsymm_1 {α : Type u_1} (r : ααProp) [inst : ] :
IsAsymm α r
Equations
theorem WellFoundedLT.induction {α : Type u} [inst : LT α] [inst : ] {C : αProp} (a : α) :
((x : α) → ((y : α) → y < xC y) → C x) → C a

Inducts on a well-founded < relation.

theorem WellFoundedLT.apply {α : Type u} [inst : LT α] [inst : ] (a : α) :
Acc (fun x x_1 => x < x_1) a

All values are accessible under the well-founded <.

noncomputable def WellFoundedLT.fix {α : Type u} [inst : LT α] [inst : ] {C : αSort u_1} :
((x : α) → ((y : α) → y < xC y) → C x) → (x : α) → C x

Creates data, given a way to generate a value from all that compare as lesser. See also WellFoundedLT.fix_eq.

Equations
theorem WellFoundedLT.fix_eq {α : Type u} [inst : LT α] [inst : ] {C : αSort u_1} (F : (x : α) → ((y : α) → y < xC y) → C x) (x : α) :
= F x fun y x =>

The value from WellFoundedLT.fix is built from the previous ones as specified.

def WellFoundedLT.toWellFoundedRelation {α : Type u} [inst : LT α] [inst : ] :

Derive a WellFoundedRelation instance from a WellFoundedLT instance.

Equations
theorem WellFoundedGT.induction {α : Type u} [inst : LT α] [inst : ] {C : αProp} (a : α) :
((x : α) → ((y : α) → x < yC y) → C x) → C a

Inducts on a well-founded > relation.

theorem WellFoundedGT.apply {α : Type u} [inst : LT α] [inst : ] (a : α) :
Acc (fun x x_1 => x > x_1) a

All values are accessible under the well-founded >.

noncomputable def WellFoundedGT.fix {α : Type u} [inst : LT α] [inst : ] {C : αSort u_1} :
((x : α) → ((y : α) → x < yC y) → C x) → (x : α) → C x

Creates data, given a way to generate a value from all that compare as greater. See also WellFoundedGT.fix_eq.

Equations
theorem WellFoundedGT.fix_eq {α : Type u} [inst : LT α] [inst : ] {C : αSort u_1} (F : (x : α) → ((y : α) → x < yC y) → C x) (x : α) :
= F x fun y x =>

The value from WellFoundedGT.fix is built from the successive ones as specified.

def WellFoundedGT.toWellFoundedRelation {α : Type u} [inst : LT α] [inst : ] :

Derive a WellFoundedRelation instance from a WellFoundedGT instance.

Equations
noncomputable def IsWellOrder.linearOrder {α : Type u} (r : ααProp) [inst : ] :

Construct a decidable linear order from a well-founded linear order.

Equations
def IsWellOrder.toHasWellFounded {α : Type u} [inst : LT α] [hwo : IsWellOrder α fun x x_1 => x < x_1] :

Derive a WellFoundedRelation instance from a IsWellOrder instance.

Equations
• IsWellOrder.toHasWellFounded = { rel := fun x x_1 => x < x_1, wf := (_ : WellFounded fun x x_1 => x < x_1) }
theorem Subsingleton.isWellOrder {α : Type u} [inst : ] (r : ααProp) [hr : IsIrrefl α r] :
instance instIsWellOrderEmptyRelation {α : Type u} [inst : ] :
IsWellOrder α EmptyRelation
Equations
instance instIsWellOrder {α : Type u} [inst : ] (r : ααProp) :
Equations
instance instIsWellFoundedProdLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [inst : ] [inst : ] :
IsWellFounded (α × β) (Prod.Lex r s)
Equations
instance instIsWellOrderProdLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [inst : ] [inst : ] :
IsWellOrder (α × β) (Prod.Lex r s)
Equations
instance instIsWellFoundedInvImage {α : Type u} {β : Type v} (r : ααProp) [inst : ] (f : βα) :
Equations
instance instIsWellFoundedMeasure {α : Type u} (f : α) :
Equations
theorem Subrelation.isWellFounded {α : Type u} (r : ααProp) [inst : ] {s : ααProp} (h : ) :
def Set.Unbounded {α : Type u} (r : ααProp) (s : Set α) :

An unbounded or cofinal set.

Equations
def Set.Bounded {α : Type u} (r : ααProp) (s : Set α) :

A bounded or final set. Not to be confused with Metric.bounded.

Equations
• = a, (b : α) → b sr b a
@[simp]
theorem Set.not_bounded_iff {α : Type u} {r : ααProp} (s : Set α) :
@[simp]
theorem Set.not_unbounded_iff {α : Type u} {r : ααProp} (s : Set α) :
theorem Set.unbounded_of_isEmpty {α : Type u} [inst : ] {r : ααProp} (s : Set α) :
instance Prod.isRefl_preimage_fst {α : Type u} {r : ααProp} [inst : IsRefl α r] :
IsRefl (α × α) (Prod.fst ⁻¹'o r)
Equations
instance Prod.isRefl_preimage_snd {α : Type u} {r : ααProp} [inst : IsRefl α r] :
IsRefl (α × α) (Prod.snd ⁻¹'o r)
Equations
instance Prod.isTrans_preimage_fst {α : Type u} {r : ααProp} [inst : IsTrans α r] :
IsTrans (α × α) (Prod.fst ⁻¹'o r)
Equations
instance Prod.isTrans_preimage_snd {α : Type u} {r : ααProp} [inst : IsTrans α r] :
IsTrans (α × α) (Prod.snd ⁻¹'o r)
Equations

### Strict-non strict relations #

class IsNonstrictStrictOrder (α : Type u_1) (r : ααProp) (s : ααProp) :
• 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

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 (⊂)⊂).

Instances
theorem right_iff_left_not_left {α : Type u} {r : ααProp} {s : ααProp} [inst : ] {a : α} {b : α} :
s a b r a b ¬r b a
theorem right_iff_left_not_left_of {α : Type u} (r : ααProp) (s : ααProp) [inst : ] {a : α} {b : α} :
s a b r a b ¬r b a

A version of right_iff_left_not_left with explicit r and s.

instance instIsIrrefl_2 {α : Type u} {r : ααProp} {s : ααProp} [inst : ] :
Equations

#### ⊆⊆ and ⊂⊂#

theorem subset_of_eq_of_subset {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b c) :
a c
theorem subset_of_subset_of_eq {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a b) (hbc : b = c) :
a c
theorem subset_refl {α : Type u} [inst : ] [inst : IsRefl α fun x x_1 => x x_1] (a : α) :
a a
theorem subset_rfl {α : Type u} [inst : ] {a : α} [inst : IsRefl α fun x x_1 => x x_1] :
a a
theorem subset_of_eq {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] :
a = ba b
theorem superset_of_eq {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] :
a = bb a
theorem ne_of_not_subset {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] :
¬a ba b
theorem ne_of_not_superset {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] :
¬a bb a
theorem subset_trans {α : Type u} [inst : ] [inst : IsTrans α fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
a bb ca c
theorem subset_antisymm {α : Type u} [inst : ] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] :
a bb aa = b
theorem superset_antisymm {α : Type u} [inst : ] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] :
a bb ab = a
theorem Eq.trans_subset {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b c) :
a c

Alias of subset_of_eq_of_subset.

theorem HasSubset.subset.trans_eq {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a b) (hbc : b = c) :
a c

Alias of subset_of_subset_of_eq.

theorem Eq.subset' {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] :
a = ba b

Alias of subset_of_eq.

theorem Eq.superset {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] :
a = bb a

Alias of superset_of_eq.

theorem HasSubset.Subset.trans {α : Type u} [inst : ] [inst : IsTrans α fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
a bb ca c

Alias of subset_trans.

theorem HasSubset.Subset.antisymm {α : Type u} [inst : ] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] :
a bb aa = b

Alias of subset_antisymm.

theorem HasSubset.Subset.antisymm' {α : Type u} [inst : ] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] :
a bb ab = a

Alias of superset_antisymm.

theorem subset_antisymm_iff {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] [inst : IsAntisymm α fun x x_1 => x x_1] :
a = b a b b a
theorem superset_antisymm_iff {α : Type u} [inst : ] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] [inst : IsAntisymm α fun x x_1 => x x_1] :
a = b b a a b
theorem ssubset_of_eq_of_ssubset {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b c) :
a c
theorem ssubset_of_ssubset_of_eq {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a b) (hbc : b = c) :
a c
theorem ssubset_irrefl {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] (a : α) :
¬a a
theorem ssubset_irrfl {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] {a : α} :
¬a a
theorem ne_of_ssubset {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] {a : α} {b : α} :
a ba b
theorem ne_of_ssuperset {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] {a : α} {b : α} :
a bb a
theorem ssubset_trans {α : Type u} [inst : ] [inst : IsTrans α fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
a bb ca c
theorem ssubset_asymm {α : Type u} [inst : ] [inst : IsAsymm α fun x x_1 => x x_1] {a : α} {b : α} :
a b¬b a
theorem Eq.trans_ssubset {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b c) :
a c

Alias of ssubset_of_eq_of_ssubset.

theorem HasSSubset.SSubset.trans_eq {α : Type u} [inst : ] {a : α} {b : α} {c : α} (hab : a b) (hbc : b = c) :
a c

Alias of ssubset_of_ssubset_of_eq.

theorem HasSSubset.SSubset.false {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] {a : α} :
¬a a

Alias of ssubset_irrfl.

theorem HasSSubset.SSubset.ne {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] {a : α} {b : α} :
a ba b

Alias of ne_of_ssubset.

theorem HasSSubset.SSubset.ne' {α : Type u} [inst : ] [inst : IsIrrefl α fun x x_1 => x x_1] {a : α} {b : α} :
a bb a

Alias of ne_of_ssuperset.

theorem HasSSubset.SSubset.trans {α : Type u} [inst : ] [inst : IsTrans α fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
a bb ca c

Alias of ssubset_trans.

theorem HasSSubset.SSubset.asymm {α : Type u} [inst : ] [inst : IsAsymm α fun x x_1 => x x_1] {a : α} {b : α} :
a b¬b a

Alias of ssubset_asymm.

theorem ssubset_iff_subset_not_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} :
a b a b ¬b a
theorem subset_of_ssubset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) :
a b
theorem not_subset_of_ssubset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) :
¬b a
theorem not_ssubset_of_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) :
¬b a
theorem ssubset_of_subset_not_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h₁ : a b) (h₂ : ¬b a) :
a b
theorem HasSSubset.SSubset.subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) :
a b

Alias of subset_of_ssubset.

theorem HasSSubset.SSubset.not_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) :
¬b a

Alias of not_subset_of_ssubset.

theorem HasSubset.Subset.not_ssubset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) :
¬b a

Alias of not_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_of_not_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} (h₁ : a b) (h₂ : ¬b a) :
a b

Alias of ssubset_of_subset_not_subset.

theorem ssubset_of_subset_of_ssubset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} [inst : IsTrans α fun x x_1 => x x_1] (h₁ : a b) (h₂ : b c) :
a c
theorem ssubset_of_ssubset_of_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} [inst : IsTrans α fun x x_1 => x x_1] (h₁ : a b) (h₂ : b c) :
a c
theorem ssubset_of_subset_of_ne {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h₁ : a b) (h₂ : a b) :
a b
theorem ssubset_of_ne_of_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h₁ : a b) (h₂ : a b) :
a b
theorem eq_or_ssubset_of_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h : a b) :
a = b a b
theorem ssubset_or_eq_of_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h : a b) :
a b a = b
theorem HasSubset.Subset.trans_ssubset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} [inst : IsTrans α fun x x_1 => x x_1] (h₁ : a b) (h₂ : b c) :
a c

Alias of ssubset_of_subset_of_ssubset.

theorem HasSSubset.SSubset.trans_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} [inst : IsTrans α fun x x_1 => x x_1] (h₁ : a b) (h₂ : b c) :
a c

Alias of ssubset_of_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_of_ne {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h₁ : a b) (h₂ : a b) :
a b

Alias of ssubset_of_subset_of_ne.

theorem Ne.ssubset_of_subset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h₁ : a b) (h₂ : a b) :
a b

Alias of ssubset_of_ne_of_subset.

theorem HasSubset.Subset.eq_or_ssubset {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h : a b) :
a = b a b

Alias of eq_or_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_or_eq {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] (h : a b) :
a b a = b

Alias of ssubset_or_eq_of_subset.

theorem ssubset_iff_subset_ne {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x x_1] :
a b a b a b
theorem subset_iff_ssubset_or_eq {α : Type u} [inst : ] [inst : ] [inst : IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x x_1] [inst : IsAntisymm α fun x x_1 => x x_1] :
a b a b a = b

### Conversion of bundled order typeclasses to unbundled relation typeclasses #

instance instIsReflLeToLE {α : Type u} [inst : ] :
IsRefl α fun x x_1 => x x_1
Equations
instance instIsReflGeToLE {α : Type u} [inst : ] :
IsRefl α fun x x_1 => x x_1
Equations
instance instIsTransLeToLE {α : Type u} [inst : ] :
IsTrans α fun x x_1 => x x_1
Equations
instance instIsTransGeToLE {α : Type u} [inst : ] :
IsTrans α fun x x_1 => x x_1
Equations
instance instIsPreorderLeToLE {α : Type u} [inst : ] :
IsPreorder α fun x x_1 => x x_1
Equations
instance instIsPreorderGeToLE {α : Type u} [inst : ] :
IsPreorder α fun x x_1 => x x_1
Equations
instance instIsIrreflLtToLT {α : Type u} [inst : ] :
IsIrrefl α fun x x_1 => x < x_1
Equations
instance instIsIrreflGtToLT {α : Type u} [inst : ] :
IsIrrefl α fun x x_1 => x > x_1
Equations
instance instIsTransLtToLT {α : Type u} [inst : ] :
IsTrans α fun x x_1 => x < x_1
Equations
instance instIsTransGtToLT {α : Type u} [inst : ] :
IsTrans α fun x x_1 => x > x_1
Equations
instance instIsAsymmLtToLT {α : Type u} [inst : ] :
IsAsymm α fun x x_1 => x < x_1
Equations
instance instIsAsymmGtToLT {α : Type u} [inst : ] :
IsAsymm α fun x x_1 => x > x_1
Equations
instance instIsAntisymmLtToLT {α : Type u} [inst : ] :
IsAntisymm α fun x x_1 => x < x_1
Equations
instance instIsAntisymmGtToLT {α : Type u} [inst : ] :
IsAntisymm α fun x x_1 => x > x_1
Equations
instance instIsStrictOrderLtToLT {α : Type u} [inst : ] :
IsStrictOrder α fun x x_1 => x < x_1
Equations
instance instIsStrictOrderGtToLT {α : Type u} [inst : ] :
IsStrictOrder α fun x x_1 => x > x_1
Equations
instance instIsNonstrictStrictOrderLeToLELtToLT {α : Type u} [inst : ] :
IsNonstrictStrictOrder α (fun x x_1 => x x_1) fun x x_1 => x < x_1
Equations
• instIsNonstrictStrictOrderLeToLELtToLT = { right_iff_left_not_left := (_ : ∀ {a b : α}, a < b a b ¬b a) }
instance instIsAntisymmLeToLEToPreorder {α : Type u} [inst : ] :
IsAntisymm α fun x x_1 => x x_1
Equations
instance instIsAntisymmGeToLEToPreorder {α : Type u} [inst : ] :
IsAntisymm α fun x x_1 => x x_1
Equations
instance instIsPartialOrderLeToLEToPreorder {α : Type u} [inst : ] :
IsPartialOrder α fun x x_1 => x x_1
Equations
instance instIsPartialOrderGeToLEToPreorder {α : Type u} [inst : ] :
IsPartialOrder α fun x x_1 => x x_1
Equations
instance instIsTotalLeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTotal α fun x x_1 => x x_1
Equations
instance instIsTotalGeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTotal α fun x x_1 => x x_1
Equations
instance instIsTotalPreorderLeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTotalPreorder α fun x x_1 => x x_1
Equations
instance instIsTotalPreorderGeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTotalPreorder α fun x x_1 => x x_1
Equations
instance instIsLinearOrderLeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsLinearOrder α fun x x_1 => x x_1
Equations
instance instIsLinearOrderGeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsLinearOrder α fun x x_1 => x x_1
Equations
instance instIsTrichotomousLtToLTToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTrichotomous α fun x x_1 => x < x_1
Equations
instance instIsTrichotomousGtToLTToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTrichotomous α fun x x_1 => x > x_1
Equations
instance instIsTrichotomousLeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTrichotomous α fun x x_1 => x x_1
Equations
instance instIsTrichotomousGeToLEToPreorderToPartialOrder {α : Type u} [inst : ] :
IsTrichotomous α fun x x_1 => x x_1
Equations
instance instIsStrictTotalOrderLtToLTToPreorderToPartialOrder {α : Type u} [inst : ] :
IsStrictTotalOrder α fun x x_1 => x < x_1
Equations
instance instIsOrderConnectedLtToLTToPreorderToPartialOrder {α : Type u} [inst : ] :
IsOrderConnected α fun x x_1 => x < x_1
Equations
instance instIsIncompTransLtToLTToPreorderToPartialOrder {α : Type u} [inst : ] :
IsIncompTrans α fun x x_1 => x < x_1
Equations
instance instIsStrictWeakOrderLtToLTToPreorderToPartialOrder {α : Type u} [inst : ] :
IsStrictWeakOrder α fun x x_1 => x < x_1
Equations
theorem transitive_le {α : Type u} [inst : ] :
theorem transitive_lt {α : Type u} [inst : ] :
theorem transitive_ge {α : Type u} [inst : ] :
theorem transitive_gt {α : Type u} [inst : ] :
instance OrderDual.isTotal_le {α : Type u} [inst : LE α] [h : IsTotal α fun x x_1 => x x_1] :
IsTotal αᵒᵈ fun x x_1 => x x_1
Equations
instance Nat.lt.isWellOrder :
IsWellOrder fun x x_1 => x < x_1
Equations
instance instIsWellOrderOrderDualGtInstLTOrderDualToLTToPreorderToPartialOrder {α : Type u} [inst : ] [h : IsWellOrder α fun x x_1 => x < x_1] :
IsWellOrder αᵒᵈ fun x x_1 => x > x_1
Equations
instance instIsWellOrderOrderDualLtInstLTOrderDualToLTToPreorderToPartialOrder {α : Type u} [inst : ] [h : IsWellOrder α fun x x_1 => x > x_1] :
IsWellOrder αᵒᵈ fun x x_1 => x < x_1
Equations