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 = b → r 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 : IsAntisymm α r] {a : α} {b : α} :

r a b → r b a → b = a

theorem antisymm_iff {α : Type u} {r : α → α → Prop} [inst : IsRefl α r] [inst : IsAntisymm α r] {a : α} {b : α} :

r a b ∧ r b a ↔ a = b

@[elab_without_expected_type]

theorem antisymm_of {α : Type u} (r : α → α → Prop) [inst : IsAntisymm α r] {a : α} {b : α} :

r a b → r b a → a = 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 : IsAntisymm α r] {a : α} {b : α} :

r a b → r b a → b = 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 α (Function.swap r)

theorem IsIrrefl.swap {α : Type u} (r : α → α → Prop) [inst : IsIrrefl α r] :

IsIrrefl α (Function.swap r)

theorem IsTrans.swap {α : Type u} (r : α → α → Prop) [inst : IsTrans α r] :

IsTrans α (Function.swap r)

theorem IsAntisymm.swap {α : Type u} (r : α → α → Prop) [inst : IsAntisymm α r] :

IsAntisymm α (Function.swap r)

theorem IsAsymm.swap {α : Type u} (r : α → α → Prop) [inst : IsAsymm α r] :

IsAsymm α (Function.swap r)

theorem IsTotal.swap {α : Type u} (r : α → α → Prop) [inst : IsTotal α r] :

IsTotal α (Function.swap r)

theorem IsTrichotomous.swap {α : Type u} (r : α → α → Prop) [inst : IsTrichotomous α r] :

IsTrichotomous α (Function.swap r)

theorem IsPreorder.swap {α : Type u} (r : α → α → Prop) [inst : IsPreorder α r] :

IsPreorder α (Function.swap r)

theorem IsStrictOrder.swap {α : Type u} (r : α → α → Prop) [inst : IsStrictOrder α r] :

IsStrictOrder α (Function.swap r)

theorem IsPartialOrder.swap {α : Type u} (r : α → α → Prop) [inst : IsPartialOrder α r] :

IsPartialOrder α (Function.swap r)

theorem IsTotalPreorder.swap {α : Type u} (r : α → α → Prop) [inst : IsTotalPreorder α r] :

IsTotalPreorder α (Function.swap r)

theorem IsLinearOrder.swap {α : Type u} (r : α → α → Prop) [inst : IsLinearOrder α r] :

IsLinearOrder α (Function.swap r)

theorem IsAsymm.isAntisymm {α : Type u} (r : α → α → Prop) [inst : IsAsymm α r] :

IsAntisymm α r

theorem IsAsymm.isIrrefl {α : Type u} {r : α → α → Prop} [inst : IsAsymm α r] :

theorem IsTotal.isTrichotomous {α : Type u} (r : α → α → Prop) [inst : IsTotal α r] :

IsTrichotomous α r

instance IsTotal.to_isRefl {α : Type u} (r : α → α → Prop) [inst : IsTotal α r] :

Equations

@IsTotal.to_isRefl = @IsTotal.to_isRefl.proof_1

theorem ne_of_irrefl {α : Type u} {r : α → α → Prop} [inst : IsIrrefl α r] {x : α} {y : α} :

r x y → x ≠ y

theorem ne_of_irrefl' {α : Type u} {r : α → α → Prop} [inst : IsIrrefl α r] {x : α} {y : α} :

r x y → y ≠ x

theorem not_rel_of_subsingleton {α : Type u} (r : α → α → Prop) [inst : IsIrrefl α r] [inst : Subsingleton α] (x : α) (y : α) :

¬r x y

theorem rel_of_subsingleton {α : Type u} (r : α → α → Prop) [inst : IsRefl α r] [inst : Subsingleton α] (x : α) (y : α) :

r x y

@[simp]

theorem empty_relation_apply {α : Type u} (a : α) (b : α) :

EmptyRelation a b ↔ False

theorem eq_empty_relation {α : Type u} (r : α → α → Prop) [inst : IsIrrefl α r] [inst : Subsingleton α] :

r = EmptyRelation

instance instIsIrreflEmptyRelation {α : Type u} :

IsIrrefl α EmptyRelation

Equations

@instIsIrreflEmptyRelation = @instIsIrreflEmptyRelation.proof_1

theorem trans_trichotomous_left {α : Type u} {r : α → α → Prop} [inst : IsTrans α r] [inst : IsTrichotomous α r] {a : α} {b : α} {c : α} :

¬r b a → r b c → r a c

theorem trans_trichotomous_right {α : Type u} {r : α → α → Prop} [inst : IsTrans α r] [inst : IsTrichotomous α r] {a : α} {b : α} {c : α} :

r a b → ¬r c b → r a c

theorem transitive_of_trans {α : Type u} (r : α → α → Prop) [inst : IsTrans α r] :

theorem extensional_of_trichotomous_of_irrefl {α : Type u} (r : α → α → Prop) [inst : IsTrichotomous α r] [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 : IsStrictOrder α r] :

PartialOrder α

Construct a partial order from a isStrictOrder relation.

See note [reducible non-instances].

Equations

partialOrderOfSO r = PartialOrder.mk (_ : ∀ (x y : α), x ≤ y → y ≤ x → x = y)

def linearOrderOfSTO {α : Type u} (r : α → α → Prop) [inst : IsStrictTotalOrder α r] [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 : IsStrictTotalOrder α r] :

IsStrictTotalOrder α (Function.swap r)

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 c → lt 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 : IsOrderConnected α r] {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 : IsOrderConnected α r] :

IsStrictWeakOrder α r

instance isStrictOrderConnected_of_isStrictTotalOrder {α : Type u} {r : α → α → Prop} [inst : IsStrictTotalOrder α r] :

IsOrderConnected α r

Equations

@isStrictOrderConnected_of_isStrictTotalOrder = @isStrictOrderConnected_of_isStrictTotalOrder.proof_1

instance isStrictTotalOrder_of_isStrictTotalOrder {α : Type u} {r : α → α → Prop} [inst : IsStrictTotalOrder α r] :

IsStrictWeakOrder α r

Equations

@isStrictTotalOrder_of_isStrictTotalOrder = @isStrictTotalOrder_of_isStrictTotalOrder.proof_1

Well-order #

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

IsWellFounded α r ↔ WellFounded r

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

The relation is WellFounded, as a proposition.
wf : WellFounded r

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

Instances

instance instIsWellFoundedRel {α : Type u} [h : WellFoundedRelation α] :

IsWellFounded α WellFoundedRelation.rel

Equations

@instIsWellFoundedRel = @instIsWellFoundedRel.proof_1

theorem WellFoundedRelation.asymmetric {α : Sort u_1} [inst : WellFoundedRelation α] {a : α} {b : α} :

WellFoundedRelation.rel a b → ¬WellFoundedRelation.rel b a

theorem WellFounded.prod_lex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra) (hb : WellFounded rb) :

WellFounded (Prod.Lex ra rb)

theorem IsWellFounded.induction {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] {C : α → Prop} (a : α) :

((x : α) → ((y : α) → r y x → C y) → C x) → C a

Induction on a well-founded relation.

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

Acc r a

All values are accessible under the well-founded relation.

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

((x : α) → ((y : α) → r y x → C 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

IsWellFounded.fix r = WellFounded.fix (_ : WellFounded fun y x => r y x)

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

IsWellFounded.fix r F x = F x fun y x => IsWellFounded.fix r F y

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

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

WellFoundedRelation α

Derive a WellFoundedRelation instance from an isWellFounded instance.

Equations

IsWellFounded.toWellFoundedRelation r = { rel := r, wf := (_ : WellFounded r) }

theorem WellFounded.asymmetric {α : Sort u_1} {r : α → α → Prop} (h : WellFounded r) (a : α) (b : α) :

r a b → ¬r b a

instance instIsAsymm {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] :

Equations

@instIsAsymm = @instIsAsymm.proof_1

instance instIsIrrefl {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] :

Equations

@instIsIrrefl = @instIsIrrefl.proof_1

def WellFoundedLT (α : Type u_1) [inst : LT α] :

A class for a well founded relation <.

Equations

WellFoundedLT α = IsWellFounded α fun x x_1 => x < x_1

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

A class for a well founded relation >.

Equations

WellFoundedGT α = IsWellFounded α fun x x_1 => x > x_1

instance instWellFoundedGTOrderDualInstLTOrderDual (α : Type u_1) [inst : LT α] [h : WellFoundedLT α] :

WellFoundedGT αᵒᵈ

Equations

instWellFoundedGTOrderDualInstLTOrderDual = instWellFoundedGTOrderDualInstLTOrderDual.proof_1

instance instWellFoundedLTOrderDualInstLTOrderDual (α : Type u_1) [inst : LT α] [h : WellFoundedGT α] :

WellFoundedLT αᵒᵈ

Equations

instWellFoundedLTOrderDualInstLTOrderDual = instWellFoundedLTOrderDualInstLTOrderDual.proof_1

theorem wellFoundedGT_dual_iff (α : Type u_1) [inst : LT α] :

WellFoundedGT αᵒᵈ ↔ WellFoundedLT α

theorem wellFoundedLT_dual_iff (α : Type u_1) [inst : LT α] :

WellFoundedLT αᵒᵈ ↔ WellFoundedGT α

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

A well order is a well-founded linear order.

Instances

instance instIsStrictTotalOrder {α : Type u_1} (r : α → α → Prop) [inst : IsWellOrder α r] :

IsStrictTotalOrder α r

Equations

@instIsStrictTotalOrder = @instIsStrictTotalOrder.proof_1

instance instIsTrichotomous {α : Type u_1} (r : α → α → Prop) [inst : IsWellOrder α r] :

IsTrichotomous α r

Equations

@instIsTrichotomous = @instIsTrichotomous.proof_1

instance instIsTrans_1 {α : Type u_1} (r : α → α → Prop) [inst : IsWellOrder α r] :

Equations

@instIsTrans_1 = @instIsTrans_1.proof_1

instance instIsIrrefl_1 {α : Type u_1} (r : α → α → Prop) [inst : IsWellOrder α r] :

Equations

@instIsIrrefl_1 = @instIsIrrefl_1.proof_1

instance instIsAsymm_1 {α : Type u_1} (r : α → α → Prop) [inst : IsWellOrder α r] :

Equations

@instIsAsymm_1 = @instIsAsymm_1.proof_1

theorem WellFoundedLT.induction {α : Type u} [inst : LT α] [inst : WellFoundedLT α] {C : α → Prop} (a : α) :

((x : α) → ((y : α) → y < x → C y) → C x) → C a

Inducts on a well-founded < relation.

theorem WellFoundedLT.apply {α : Type u} [inst : LT α] [inst : WellFoundedLT α] (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 : WellFoundedLT α] {C : α → Sort u_1} :

((x : α) → ((y : α) → y < x → C 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

WellFoundedLT.fix = IsWellFounded.fix fun x x_1 => x < x_1

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

WellFoundedLT.fix F x = F x fun y x => WellFoundedLT.fix F y

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

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

WellFoundedRelation α

Derive a WellFoundedRelation instance from a WellFoundedLT instance.

Equations

WellFoundedLT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun x x_1 => x < x_1

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

((x : α) → ((y : α) → x < y → C y) → C x) → C a

Inducts on a well-founded > relation.

theorem WellFoundedGT.apply {α : Type u} [inst : LT α] [inst : WellFoundedGT α] (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 : WellFoundedGT α] {C : α → Sort u_1} :

((x : α) → ((y : α) → x < y → C 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

WellFoundedGT.fix = IsWellFounded.fix fun x x_1 => x > x_1

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

WellFoundedGT.fix F x = F x fun y x => WellFoundedGT.fix F y

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

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

WellFoundedRelation α

Derive a WellFoundedRelation instance from a WellFoundedGT instance.

Equations

WellFoundedGT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun x x_1 => x > x_1

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

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

Equations

IsWellOrder.linearOrder r = linearOrderOfSTO r

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

WellFoundedRelation α

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 : Subsingleton α] (r : α → α → Prop) [hr : IsIrrefl α r] :

IsWellOrder α r

instance instIsWellOrderEmptyRelation {α : Type u} [inst : Subsingleton α] :

IsWellOrder α EmptyRelation

Equations

@instIsWellOrderEmptyRelation = @instIsWellOrderEmptyRelation.proof_1

instance instIsWellOrder {α : Type u} [inst : IsEmpty α] (r : α → α → Prop) :

IsWellOrder α r

Equations

@instIsWellOrder = @instIsWellOrder.proof_1

instance instIsWellFoundedProdLex {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellFounded α r] [inst : IsWellFounded β s] :

IsWellFounded (α × β) (Prod.Lex r s)

Equations

@instIsWellFoundedProdLex = @instIsWellFoundedProdLex.proof_1

instance instIsWellOrderProdLex {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst : IsWellOrder β s] :

IsWellOrder (α × β) (Prod.Lex r s)

Equations

@instIsWellOrderProdLex = @instIsWellOrderProdLex.proof_1

instance instIsWellFoundedInvImage {α : Type u} {β : Type v} (r : α → α → Prop) [inst : IsWellFounded α r] (f : β → α) :

IsWellFounded β (InvImage r f)

Equations

@instIsWellFoundedInvImage = @instIsWellFoundedInvImage.proof_1

instance instIsWellFoundedMeasure {α : Type u} (f : α → ℕ) :

IsWellFounded α (Measure f)

Equations

@instIsWellFoundedMeasure = @instIsWellFoundedMeasure.proof_1

theorem Subrelation.isWellFounded {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] {s : α → α → Prop} (h : Subrelation s r) :

IsWellFounded α s

def Set.Unbounded {α : Type u} (r : α → α → Prop) (s : Set α) :

An unbounded or cofinal set.

Equations

Set.Unbounded r s = ∀ (a : α), ∃ b, b ∈ s ∧ ¬r b a

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

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

Equations

Set.Bounded r s = ∃ a, (b : α) → b ∈ s → r b a

@[simp]

theorem Set.not_bounded_iff {α : Type u} {r : α → α → Prop} (s : Set α) :

¬Set.Bounded r s ↔ Set.Unbounded r s

@[simp]

theorem Set.not_unbounded_iff {α : Type u} {r : α → α → Prop} (s : Set α) :

¬Set.Unbounded r s ↔ Set.Bounded r s

theorem Set.unbounded_of_isEmpty {α : Type u} [inst : IsEmpty α] {r : α → α → Prop} (s : Set α) :

Set.Unbounded r s

instance Prod.isRefl_preimage_fst {α : Type u} {r : α → α → Prop} [inst : IsRefl α r] :

IsRefl (α × α) (Prod.fst ⁻¹'o r)

Equations

@Prod.isRefl_preimage_fst = @Prod.isRefl_preimage_fst.proof_1

instance Prod.isRefl_preimage_snd {α : Type u} {r : α → α → Prop} [inst : IsRefl α r] :

IsRefl (α × α) (Prod.snd ⁻¹'o r)

Equations

@Prod.isRefl_preimage_snd = @Prod.isRefl_preimage_snd.proof_1

instance Prod.isTrans_preimage_fst {α : Type u} {r : α → α → Prop} [inst : IsTrans α r] :

IsTrans (α × α) (Prod.fst ⁻¹'o r)

Equations

@Prod.isTrans_preimage_fst = @Prod.isTrans_preimage_fst.proof_1

instance Prod.isTrans_preimage_snd {α : Type u} {r : α → α → Prop} [inst : IsTrans α r] :

IsTrans (α × α) (Prod.snd ⁻¹'o r)

Equations

@Prod.isTrans_preimage_snd = @Prod.isTrans_preimage_snd.proof_1

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 : IsNonstrictStrictOrder α r s] {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 : IsNonstrictStrictOrder α r s] {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 : IsNonstrictStrictOrder α r s] :

Equations

@instIsIrrefl_2 = @instIsIrrefl_2.proof_1

`⊆⊆` and `⊂⊂` #

theorem subset_of_eq_of_subset {α : Type u} [inst : HasSubset α] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b ⊆ c) :

a ⊆ c

theorem subset_of_subset_of_eq {α : Type u} [inst : HasSubset α] {a : α} {b : α} {c : α} (hab : a ⊆ b) (hbc : b = c) :

a ⊆ c

theorem subset_refl {α : Type u} [inst : HasSubset α] [inst : IsRefl α fun x x_1 => x ⊆ x_1] (a : α) :

a ⊆ a

theorem subset_rfl {α : Type u} [inst : HasSubset α] {a : α} [inst : IsRefl α fun x x_1 => x ⊆ x_1] :

a ⊆ a

theorem subset_of_eq {α : Type u} [inst : HasSubset α] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x ⊆ x_1] :

a = b → a ⊆ b

theorem superset_of_eq {α : Type u} [inst : HasSubset α] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x ⊆ x_1] :

a = b → b ⊆ a

theorem ne_of_not_subset {α : Type u} [inst : HasSubset α] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x ⊆ x_1] :

¬a ⊆ b → a ≠ b

theorem ne_of_not_superset {α : Type u} [inst : HasSubset α] {a : α} {b : α} [inst : IsRefl α fun x x_1 => x ⊆ x_1] :

¬a ⊆ b → b ≠ a

theorem subset_trans {α : Type u} [inst : HasSubset α] [inst : IsTrans α fun x x_1 => x ⊆ x_1] {a : α} {b : α} {c : α} :

a ⊆ b → b ⊆ c → a ⊆ c

theorem subset_antisymm {α : Type u} [inst : HasSubset α] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x ⊆ x_1] :

a ⊆ b → b ⊆ a → a = b

theorem superset_antisymm {α : Type u} [inst : HasSubset α] {a : α} {b : α} [inst : IsAntisymm α fun x x_1 => x ⊆ x_1] :

a ⊆ b → b ⊆ a → b = a

theorem Eq.trans_subset {α : Type u} [inst : HasSubset α] {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 : HasSubset α] {a : α} {b : α} {c : α} (hab : a ⊆ b) (hbc : b = c) :

a ⊆ c

Alias of subset_of_subset_of_eq.

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

a = b → a ⊆ b

Alias of subset_of_eq.

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

a = b → b ⊆ a

Alias of superset_of_eq.

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

a ⊆ b → b ⊆ c → a ⊆ c

Alias of subset_trans.

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

a ⊆ b → b ⊆ a → a = b

Alias of subset_antisymm.

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

a ⊆ b → b ⊆ a → b = a

Alias of superset_antisymm.

theorem subset_antisymm_iff {α : Type u} [inst : HasSubset α] {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 : HasSubset α] {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 : HasSSubset α] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b ⊂ c) :

a ⊂ c

theorem ssubset_of_ssubset_of_eq {α : Type u} [inst : HasSSubset α] {a : α} {b : α} {c : α} (hab : a ⊂ b) (hbc : b = c) :

a ⊂ c

theorem ssubset_irrefl {α : Type u} [inst : HasSSubset α] [inst : IsIrrefl α fun x x_1 => x ⊂ x_1] (a : α) :

theorem ssubset_irrfl {α : Type u} [inst : HasSSubset α] [inst : IsIrrefl α fun x x_1 => x ⊂ x_1] {a : α} :

theorem ne_of_ssubset {α : Type u} [inst : HasSSubset α] [inst : IsIrrefl α fun x x_1 => x ⊂ x_1] {a : α} {b : α} :

a ⊂ b → a ≠ b

theorem ne_of_ssuperset {α : Type u} [inst : HasSSubset α] [inst : IsIrrefl α fun x x_1 => x ⊂ x_1] {a : α} {b : α} :

a ⊂ b → b ≠ a

theorem ssubset_trans {α : Type u} [inst : HasSSubset α] [inst : IsTrans α fun x x_1 => x ⊂ x_1] {a : α} {b : α} {c : α} :

a ⊂ b → b ⊂ c → a ⊂ c

theorem ssubset_asymm {α : Type u} [inst : HasSSubset α] [inst : IsAsymm α fun x x_1 => x ⊂ x_1] {a : α} {b : α} :

a ⊂ b → ¬b ⊂ a

theorem Eq.trans_ssubset {α : Type u} [inst : HasSSubset α] {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 : HasSSubset α] {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 : HasSSubset α] [inst : IsIrrefl α fun x x_1 => x ⊂ x_1] {a : α} :

Alias of ssubset_irrfl.

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

a ⊂ b → a ≠ b

Alias of ne_of_ssubset.

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

a ⊂ b → b ≠ a

Alias of ne_of_ssuperset.

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

a ⊂ b → b ⊂ c → a ⊂ c

Alias of ssubset_trans.

theorem HasSSubset.SSubset.asymm {α : Type u} [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [inst : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a : α} {b : α} (h : a ⊂ b) :

theorem not_ssubset_of_subset {α : Type u} [inst : HasSubset α] [inst : HasSSubset α] [inst : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a : α} {b : α} (h : a ⊆ b) :

theorem ssubset_of_subset_not_subset {α : Type u} [inst : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [inst : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a : α} {b : α} (h : a ⊂ b) :

Alias of not_subset_of_ssubset.

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

Alias of not_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_of_not_subset {α : Type u} [inst : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : HasSubset α] [inst : HasSSubset α] [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 : Preorder α] :

IsRefl α fun x x_1 => x ≤ x_1

Equations

@instIsReflLeToLE = @instIsReflLeToLE.proof_1

instance instIsReflGeToLE {α : Type u} [inst : Preorder α] :

IsRefl α fun x x_1 => x ≥ x_1

Equations

@instIsReflGeToLE = @instIsReflGeToLE.proof_1

instance instIsTransLeToLE {α : Type u} [inst : Preorder α] :

IsTrans α fun x x_1 => x ≤ x_1

Equations

@instIsTransLeToLE = @instIsTransLeToLE.proof_1

instance instIsTransGeToLE {α : Type u} [inst : Preorder α] :

IsTrans α fun x x_1 => x ≥ x_1

Equations

@instIsTransGeToLE = @instIsTransGeToLE.proof_1

instance instIsPreorderLeToLE {α : Type u} [inst : Preorder α] :

IsPreorder α fun x x_1 => x ≤ x_1

Equations

@instIsPreorderLeToLE = @instIsPreorderLeToLE.proof_1

instance instIsPreorderGeToLE {α : Type u} [inst : Preorder α] :

IsPreorder α fun x x_1 => x ≥ x_1

Equations

@instIsPreorderGeToLE = @instIsPreorderGeToLE.proof_1

instance instIsIrreflLtToLT {α : Type u} [inst : Preorder α] :

IsIrrefl α fun x x_1 => x < x_1

Equations

@instIsIrreflLtToLT = @instIsIrreflLtToLT.proof_1

instance instIsIrreflGtToLT {α : Type u} [inst : Preorder α] :

IsIrrefl α fun x x_1 => x > x_1

Equations

@instIsIrreflGtToLT = @instIsIrreflGtToLT.proof_1

instance instIsTransLtToLT {α : Type u} [inst : Preorder α] :

IsTrans α fun x x_1 => x < x_1

Equations

@instIsTransLtToLT = @instIsTransLtToLT.proof_1

instance instIsTransGtToLT {α : Type u} [inst : Preorder α] :

IsTrans α fun x x_1 => x > x_1

Equations

@instIsTransGtToLT = @instIsTransGtToLT.proof_1

instance instIsAsymmLtToLT {α : Type u} [inst : Preorder α] :

IsAsymm α fun x x_1 => x < x_1

Equations

@instIsAsymmLtToLT = @instIsAsymmLtToLT.proof_1

instance instIsAsymmGtToLT {α : Type u} [inst : Preorder α] :

IsAsymm α fun x x_1 => x > x_1

Equations

@instIsAsymmGtToLT = @instIsAsymmGtToLT.proof_1

instance instIsAntisymmLtToLT {α : Type u} [inst : Preorder α] :

IsAntisymm α fun x x_1 => x < x_1

Equations

@instIsAntisymmLtToLT = @instIsAntisymmLtToLT.proof_1

instance instIsAntisymmGtToLT {α : Type u} [inst : Preorder α] :

IsAntisymm α fun x x_1 => x > x_1

Equations

@instIsAntisymmGtToLT = @instIsAntisymmGtToLT.proof_1

instance instIsStrictOrderLtToLT {α : Type u} [inst : Preorder α] :

IsStrictOrder α fun x x_1 => x < x_1

Equations

@instIsStrictOrderLtToLT = @instIsStrictOrderLtToLT.proof_1

instance instIsStrictOrderGtToLT {α : Type u} [inst : Preorder α] :

IsStrictOrder α fun x x_1 => x > x_1

Equations

@instIsStrictOrderGtToLT = @instIsStrictOrderGtToLT.proof_1

instance instIsNonstrictStrictOrderLeToLELtToLT {α : Type u} [inst : Preorder α] :

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 : PartialOrder α] :

IsAntisymm α fun x x_1 => x ≤ x_1

Equations

@instIsAntisymmLeToLEToPreorder = @instIsAntisymmLeToLEToPreorder.proof_1

instance instIsAntisymmGeToLEToPreorder {α : Type u} [inst : PartialOrder α] :

IsAntisymm α fun x x_1 => x ≥ x_1

Equations

@instIsAntisymmGeToLEToPreorder = @instIsAntisymmGeToLEToPreorder.proof_1

instance instIsPartialOrderLeToLEToPreorder {α : Type u} [inst : PartialOrder α] :

IsPartialOrder α fun x x_1 => x ≤ x_1

Equations

@instIsPartialOrderLeToLEToPreorder = @instIsPartialOrderLeToLEToPreorder.proof_1

instance instIsPartialOrderGeToLEToPreorder {α : Type u} [inst : PartialOrder α] :

IsPartialOrder α fun x x_1 => x ≥ x_1

Equations

@instIsPartialOrderGeToLEToPreorder = @instIsPartialOrderGeToLEToPreorder.proof_1

instance instIsTotalLeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTotal α fun x x_1 => x ≤ x_1

Equations

@instIsTotalLeToLEToPreorderToPartialOrder = @instIsTotalLeToLEToPreorderToPartialOrder.proof_1

instance instIsTotalGeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTotal α fun x x_1 => x ≥ x_1

Equations

@instIsTotalGeToLEToPreorderToPartialOrder = @instIsTotalGeToLEToPreorderToPartialOrder.proof_1

instance instIsTotalPreorderLeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTotalPreorder α fun x x_1 => x ≤ x_1

Equations

@instIsTotalPreorderLeToLEToPreorderToPartialOrder = @instIsTotalPreorderLeToLEToPreorderToPartialOrder.proof_1

instance instIsTotalPreorderGeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTotalPreorder α fun x x_1 => x ≥ x_1

Equations

@instIsTotalPreorderGeToLEToPreorderToPartialOrder = @instIsTotalPreorderGeToLEToPreorderToPartialOrder.proof_1

instance instIsLinearOrderLeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsLinearOrder α fun x x_1 => x ≤ x_1

Equations

@instIsLinearOrderLeToLEToPreorderToPartialOrder = @instIsLinearOrderLeToLEToPreorderToPartialOrder.proof_1

instance instIsLinearOrderGeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsLinearOrder α fun x x_1 => x ≥ x_1

Equations

@instIsLinearOrderGeToLEToPreorderToPartialOrder = @instIsLinearOrderGeToLEToPreorderToPartialOrder.proof_1

instance instIsTrichotomousLtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTrichotomous α fun x x_1 => x < x_1

Equations

@instIsTrichotomousLtToLTToPreorderToPartialOrder = @instIsTrichotomousLtToLTToPreorderToPartialOrder.proof_1

instance instIsTrichotomousGtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTrichotomous α fun x x_1 => x > x_1

Equations

@instIsTrichotomousGtToLTToPreorderToPartialOrder = @instIsTrichotomousGtToLTToPreorderToPartialOrder.proof_1

instance instIsTrichotomousLeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTrichotomous α fun x x_1 => x ≤ x_1

Equations

@instIsTrichotomousLeToLEToPreorderToPartialOrder = @instIsTrichotomousLeToLEToPreorderToPartialOrder.proof_1

instance instIsTrichotomousGeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsTrichotomous α fun x x_1 => x ≥ x_1

Equations

@instIsTrichotomousGeToLEToPreorderToPartialOrder = @instIsTrichotomousGeToLEToPreorderToPartialOrder.proof_1

instance instIsStrictTotalOrderLtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsStrictTotalOrder α fun x x_1 => x < x_1

Equations

@instIsStrictTotalOrderLtToLTToPreorderToPartialOrder = @instIsStrictTotalOrderLtToLTToPreorderToPartialOrder.proof_1

instance instIsOrderConnectedLtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsOrderConnected α fun x x_1 => x < x_1

Equations

@instIsOrderConnectedLtToLTToPreorderToPartialOrder = @instIsOrderConnectedLtToLTToPreorderToPartialOrder.proof_1

instance instIsIncompTransLtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsIncompTrans α fun x x_1 => x < x_1

Equations

@instIsIncompTransLtToLTToPreorderToPartialOrder = @instIsIncompTransLtToLTToPreorderToPartialOrder.proof_1

instance instIsStrictWeakOrderLtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] :

IsStrictWeakOrder α fun x x_1 => x < x_1

Equations

@instIsStrictWeakOrderLtToLTToPreorderToPartialOrder = @instIsStrictWeakOrderLtToLTToPreorderToPartialOrder.proof_1

theorem transitive_le {α : Type u} [inst : Preorder α] :

Transitive LE.le

theorem transitive_lt {α : Type u} [inst : Preorder α] :

Transitive LT.lt

theorem transitive_ge {α : Type u} [inst : Preorder α] :

Transitive GE.ge

theorem transitive_gt {α : Type u} [inst : Preorder α] :

Transitive GT.gt

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

@OrderDual.isTotal_le = @OrderDual.isTotal_le.proof_1

instance instWellFoundedLTNatInstLTNat :

WellFoundedLT ℕ

Equations

instWellFoundedLTNatInstLTNat = instWellFoundedLTNatInstLTNat.proof_1

instance Nat.lt.isWellOrder :

IsWellOrder ℕ fun x x_1 => x < x_1

Equations

Nat.lt.isWellOrder = Nat.lt.isWellOrder.proof_1

instance instIsWellOrderOrderDualGtInstLTOrderDualToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] [h : IsWellOrder α fun x x_1 => x < x_1] :

IsWellOrder αᵒᵈ fun x x_1 => x > x_1

Equations

@instIsWellOrderOrderDualGtInstLTOrderDualToLTToPreorderToPartialOrder = @instIsWellOrderOrderDualGtInstLTOrderDualToLTToPreorderToPartialOrder.proof_1

instance instIsWellOrderOrderDualLtInstLTOrderDualToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] [h : IsWellOrder α fun x x_1 => x > x_1] :

IsWellOrder αᵒᵈ fun x x_1 => x < x_1

Equations

@instIsWellOrderOrderDualLtInstLTOrderDualToLTToPreorderToPartialOrder = @instIsWellOrderOrderDualLtInstLTOrderDualToLTToPreorderToPartialOrder.proof_1