Documentation

Mathlib.Order.RelClasses

Unbundled relation classes #

In this file we prove some properties of Is* classes defined in Mathlib.Order.Defs. 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 IsRefl.swap {α : Type u} (r : α → α → Prop) [IsRefl α r] :

IsRefl α (Function.swap r)

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

IsIrrefl α (Function.swap r)

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

IsTrans α (Function.swap r)

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

IsAntisymm α (Function.swap r)

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

IsAsymm α (Function.swap r)

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

IsTotal α (Function.swap r)

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

IsTrichotomous α (Function.swap r)

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

IsPreorder α (Function.swap r)

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

IsStrictOrder α (Function.swap r)

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

IsPartialOrder α (Function.swap r)

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

r = EmptyRelation

@[reducible, inline]

abbrev partialOrderOfSO {α : Type u} (r : α → α → Prop) [IsStrictOrder α r] :

PartialOrder α

Construct a partial order from an isStrictOrder relation.

See note [reducible non-instances].

Equations

partialOrderOfSO r = PartialOrder.mk ⋯

@[reducible, inline]

abbrev linearOrderOfSTO {α : Type u} (r : α → α → Prop) [IsStrictTotalOrder α r] [DecidableRel r] :

Construct a linear order from an IsStrictTotalOrder relation.

See note [reducible non-instances].

Equations

linearOrderOfSTO r = LinearOrder.mk ⋯ (fun (x y : α) => decidable_of_iff (¬r y x) ⋯) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

theorem IsStrictTotalOrder.swap {α : Type u} (r : α → α → Prop) [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. This is recognizable as an intuitionistic substitute for a ≤ b ∨ b ≤ a on the constructive reals, and is also known as negative transitivity, since the contrapositive asserts transitivity of the relation ¬ a < b.

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.

Instances

theorem IsOrderConnected.neg_trans {α : Type u} {r : α → α → Prop} [IsOrderConnected α r] {a b c : α} (h₁ : ¬r a b) (h₂ : ¬r b c) :

¬r a c

theorem isStrictWeakOrder_of_isOrderConnected {α : Type u} {r : α → α → Prop} [IsAsymm α r] [IsOrderConnected α r] :

IsStrictWeakOrder α r

@[instance 100]

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

IsOrderConnected α r

Inverse Image #

theorem InvImage.isTrichotomous {α : Type u} {β : Type v} {r : α → α → Prop} [IsTrichotomous α r] {f : β → α} (h : Function.Injective f) :

IsTrichotomous β (InvImage r f)

instance InvImage.isAsymm {α : Type u} {β : Type v} {r : α → α → Prop} [IsAsymm α r] (f : β → α) :

IsAsymm β (InvImage r f)

Well-order #

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

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

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

Instances

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

IsWellFounded α r ↔ WellFounded r

instance WellFoundedRelation.isWellFounded {α : Type u} [h : WellFoundedRelation α] :

IsWellFounded α rel

@[irreducible]

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

rel a b → ¬rel b a

@[irreducible]

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

rel a b → rel b c → ¬rel c 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 WellFounded.psigma_lex {α : Sort u_1} {β : α → Sort u_2} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (ha : WellFounded r) (hb : ∀ (x : α), WellFounded (s x)) :

WellFounded (PSigma.Lex r s)

The lexicographical order of well-founded relations is well-founded.

theorem WellFounded.psigma_revLex {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :

WellFounded (PSigma.RevLex r s)

theorem WellFounded.psigma_skipLeft (α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFounded s) :

WellFounded (PSigma.SkipLeft α s)

theorem IsWellFounded.induction {α : Type u} (r : α → α → Prop) [IsWellFounded α r] {C : α → Prop} (a : α) (ind : ∀ (x : α), (∀ (y : α), r y x → C y) → C x) :

C a

Induction on a well-founded relation.

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

Acc r a

All values are accessible under the well-founded relation.

def IsWellFounded.fix {α : Type u} (r : α → α → Prop) [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 = ⋯.fix

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

fix r F x = F x fun (y : α) (x : r y x) => fix r F y

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

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

WellFoundedRelation α

Derive a WellFoundedRelation instance from an isWellFounded instance.

Equations

IsWellFounded.toWellFoundedRelation r = { rel := r, wf := ⋯ }

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

r a b → ¬r b a

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

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

@[instance 100]

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

@[instance 100]

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

instance instIsWellFoundedTransGen {α : Type u} (r : α → α → Prop) [i : IsWellFounded α r] :

IsWellFounded α (Relation.TransGen r)

@[reducible, inline]

abbrev WellFoundedLT (α : Type u_1) [LT α] :

A class for a well founded relation <.

Equations

WellFoundedLT α = IsWellFounded α fun (x1 x2 : α) => x1 < x2

@[reducible, inline]

abbrev WellFoundedGT (α : Type u_1) [LT α] :

A class for a well founded relation >.

Equations

WellFoundedGT α = IsWellFounded α fun (x1 x2 : α) => x1 > x2

theorem wellFounded_lt {α : Type u} [LT α] [WellFoundedLT α] :

WellFounded fun (x1 x2 : α) => x1 < x2

theorem wellFounded_gt {α : Type u} [LT α] [WellFoundedGT α] :

WellFounded fun (x1 x2 : α) => x1 > x2

@[instance 100]

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

WellFoundedGT αᵒᵈ

@[instance 100]

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

WellFoundedLT αᵒᵈ

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

WellFoundedGT αᵒᵈ ↔ WellFoundedLT α

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

WellFoundedLT αᵒᵈ ↔ WellFoundedGT α

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

A well order is a well-founded linear order.

trichotomous (a b : α) : r a b ∨ a = b ∨ r b a
trans (a b c : α) : r a b → r b c → r a c
wf : WellFounded r

Instances

@[instance 100]

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

IsStrictTotalOrder α r

@[instance 100]

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

IsTrichotomous α r

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

theorem WellFoundedLT.induction {α : Type u} [LT α] [WellFoundedLT α] {C : α → Prop} (a : α) (ind : ∀ (x : α), (∀ (y : α), y < x → C y) → C x) :

C a

Inducts on a well-founded < relation.

theorem WellFoundedLT.apply {α : Type u} [LT α] [WellFoundedLT α] (a : α) :

Acc (fun (x1 x2 : α) => x1 < x2) a

All values are accessible under the well-founded <.

def WellFoundedLT.fix {α : Type u} [LT α] [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 (x1 x2 : α) => x1 < x2

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

fix F x = F x fun (y : α) (x : y < x) => fix F y

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

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

WellFoundedRelation α

Derive a WellFoundedRelation instance from a WellFoundedLT instance.

Equations

WellFoundedLT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun (x1 x2 : α) => x1 < x2

theorem WellFoundedGT.induction {α : Type u} [LT α] [WellFoundedGT α] {C : α → Prop} (a : α) (ind : ∀ (x : α), (∀ (y : α), x < y → C y) → C x) :

C a

Inducts on a well-founded > relation.

theorem WellFoundedGT.apply {α : Type u} [LT α] [WellFoundedGT α] (a : α) :

Acc (fun (x1 x2 : α) => x1 > x2) a

All values are accessible under the well-founded >.

def WellFoundedGT.fix {α : Type u} [LT α] [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 (x1 x2 : α) => x1 > x2

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

fix F x = F x fun (y : α) (x : x < y) => fix F y

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

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

WellFoundedRelation α

Derive a WellFoundedRelation instance from a WellFoundedGT instance.

Equations

WellFoundedGT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun (x1 x2 : α) => x1 > x2

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

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

Equations

IsWellOrder.linearOrder r = linearOrderOfSTO r

def IsWellOrder.toHasWellFounded {α : Type u} [LT α] [hwo : IsWellOrder α fun (x1 x2 : α) => x1 < x2] :

WellFoundedRelation α

Derive a WellFoundedRelation instance from an IsWellOrder instance.

Equations

IsWellOrder.toHasWellFounded = { rel := fun (x1 x2 : α) => x1 < x2, wf := ⋯ }

theorem Subsingleton.isWellOrder {α : Type u} [Subsingleton α] (r : α → α → Prop) [hr : IsIrrefl α r] :

IsWellOrder α r

instance instIsWellOrderEmptyRelationOfSubsingleton {α : Type u} [Subsingleton α] :

IsWellOrder α EmptyRelation

@[instance 100]

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

IsWellOrder α r

instance Prod.Lex.instIsWellFounded {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellFounded α r] [IsWellFounded β s] :

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

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

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

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

IsWellFounded β (InvImage r f)

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

IsWellFounded α (InvImage (fun (x1 x2 : ℕ) => x1 < x2) f)

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

IsWellFounded α s

theorem Prod.wellFoundedLT' {α : Type u} {β : Type v} [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] :

WellFoundedLT (α × β)

See Prod.wellFoundedLT for a version that only requires Preorder α.

theorem Prod.wellFoundedGT' {α : Type u} {β : Type v} [PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] :

WellFoundedGT (α × β)

See Prod.wellFoundedGT for a version that only requires Preorder α.

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 Bornology.IsBounded.

Equations

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

@[simp]

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

¬Bounded r s ↔ Unbounded r s

@[simp]

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

¬Unbounded r s ↔ Bounded r s

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

instance Order.Preimage.instIsRefl {α : Type u} {β : Type v} {r : α → α → Prop} [IsRefl α r] {f : β → α} :

IsRefl β (f ⁻¹'o r)

instance Order.Preimage.instIsIrrefl {α : Type u} {β : Type v} {r : α → α → Prop} [IsIrrefl α r] {f : β → α} :

IsIrrefl β (f ⁻¹'o r)

instance Order.Preimage.instIsSymm {α : Type u} {β : Type v} {r : α → α → Prop} [IsSymm α r] {f : β → α} :

IsSymm β (f ⁻¹'o r)

instance Order.Preimage.instIsAsymm {α : Type u} {β : Type v} {r : α → α → Prop} [IsAsymm α r] {f : β → α} :

IsAsymm β (f ⁻¹'o r)

instance Order.Preimage.instIsTrans {α : Type u} {β : Type v} {r : α → α → Prop} [IsTrans α r] {f : β → α} :

IsTrans β (f ⁻¹'o r)

instance Order.Preimage.instIsPreorder {α : Type u} {β : Type v} {r : α → α → Prop} [IsPreorder α r] {f : β → α} :

IsPreorder β (f ⁻¹'o r)

instance Order.Preimage.instIsStrictOrder {α : Type u} {β : Type v} {r : α → α → Prop} [IsStrictOrder α r] {f : β → α} :

IsStrictOrder β (f ⁻¹'o r)

instance Order.Preimage.instIsStrictWeakOrder {α : Type u} {β : Type v} {r : α → α → Prop} [IsStrictWeakOrder α r] {f : β → α} :

IsStrictWeakOrder β (f ⁻¹'o r)

instance Order.Preimage.instIsEquiv {α : Type u} {β : Type v} {r : α → α → Prop} [IsEquiv α r] {f : β → α} :

IsEquiv β (f ⁻¹'o r)

instance Order.Preimage.instIsTotal {α : Type u} {β : Type v} {r : α → α → Prop} [IsTotal α r] {f : β → α} :

IsTotal β (f ⁻¹'o r)

theorem Order.Preimage.isAntisymm {α : Type u} {β : Type v} {r : α → α → Prop} [IsAntisymm α r] {f : β → α} (hf : Function.Injective f) :

IsAntisymm β (f ⁻¹'o r)

Strict-non strict relations #

class IsNonstrictStrictOrder (α : Type u_1) (r : semiOutParam (α → α → Prop)) (s : α → α → Prop) :

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

right_iff_left_not_left (a b : α) : s a b ↔ r a b ∧ ¬r b a
The relation r is the nonstrict relation corresponding to the strict relation s.

Instances

theorem right_iff_left_not_left {α : Type u} {r s : α → α → Prop} [IsNonstrictStrictOrder α r s] {a b : α} :

s a b ↔ r a b ∧ ¬r b a

theorem right_iff_left_not_left_of {α : Type u} (r s : α → α → Prop) [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 instIsIrreflOfIsNonstrictStrictOrder {α : Type u} {r s : α → α → Prop} [IsNonstrictStrictOrder α r s] :

`⊆` and `⊂` #

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

a ⊆ c

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

a ⊆ c

@[simp]

theorem subset_refl {α : Type u} [HasSubset α] [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] (a : α) :

a ⊆ a

theorem subset_rfl {α : Type u} [HasSubset α] {a : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊆ a

theorem subset_of_eq {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

a = b → a ⊆ b

theorem superset_of_eq {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

a = b → b ⊆ a

theorem ne_of_not_subset {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

¬a ⊆ b → a ≠ b

theorem ne_of_not_superset {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

¬a ⊆ b → b ≠ a

theorem subset_trans {α : Type u} [HasSubset α] [IsTrans α fun (x1 x2 : α) => x1 ⊆ x2] {a b c : α} :

a ⊆ b → b ⊆ c → a ⊆ c

theorem subset_antisymm {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊆ b → b ⊆ a → a = b

theorem superset_antisymm {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊆ b → b ⊆ a → b = a

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

a ⊆ c

Alias of subset_of_subset_of_eq.

theorem Eq.subset' {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

a = b → a ⊆ b

Alias of subset_of_eq.

theorem Eq.superset {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] :

a = b → b ⊆ a

Alias of superset_of_eq.

theorem HasSubset.Subset.trans {α : Type u} [HasSubset α] [IsTrans α fun (x1 x2 : α) => x1 ⊆ x2] {a b c : α} :

a ⊆ b → b ⊆ c → a ⊆ c

Alias of subset_trans.

theorem HasSubset.Subset.antisymm {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊆ b → b ⊆ a → a = b

Alias of subset_antisymm.

theorem HasSubset.Subset.antisymm' {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊆ b → b ⊆ a → b = a

Alias of superset_antisymm.

theorem subset_antisymm_iff {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a = b ↔ a ⊆ b ∧ b ⊆ a

theorem superset_antisymm_iff {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a = b ↔ b ⊆ a ∧ a ⊆ b

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

a ⊂ c

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

a ⊂ c

theorem ssubset_irrefl {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] (a : α) :

theorem ssubset_irrfl {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] {a : α} :

theorem ne_of_ssubset {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

a ⊂ b → a ≠ b

theorem ne_of_ssuperset {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

a ⊂ b → b ≠ a

theorem ssubset_trans {α : Type u} [HasSSubset α] [IsTrans α fun (x1 x2 : α) => x1 ⊂ x2] {a b c : α} :

a ⊂ b → b ⊂ c → a ⊂ c

theorem ssubset_asymm {α : Type u} [HasSSubset α] [IsAsymm α fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

a ⊂ b → ¬b ⊂ a

theorem Eq.trans_ssubset {α : Type u} [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} [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} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] {a : α} :

Alias of ssubset_irrfl.

theorem HasSSubset.SSubset.ne {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

a ⊂ b → a ≠ b

Alias of ne_of_ssubset.

theorem HasSSubset.SSubset.ne' {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

a ⊂ b → b ≠ a

Alias of ne_of_ssuperset.

theorem HasSSubset.SSubset.trans {α : Type u} [HasSSubset α] [IsTrans α fun (x1 x2 : α) => x1 ⊂ x2] {a b c : α} :

a ⊂ b → b ⊂ c → a ⊂ c

Alias of ssubset_trans.

theorem HasSSubset.SSubset.asymm {α : Type u} [HasSSubset α] [IsAsymm α fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

a ⊂ b → ¬b ⊂ a

Alias of ssubset_asymm.

theorem ssubset_iff_subset_not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} :

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

theorem subset_of_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} (h : a ⊂ b) :

a ⊆ b

theorem not_subset_of_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} (h : a ⊂ b) :

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

theorem ssubset_of_subset_not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} (h₁ : a ⊆ b) (h₂ : ¬b ⊆ a) :

a ⊂ b

theorem HasSSubset.SSubset.subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} (h : a ⊂ b) :

a ⊆ b

Alias of subset_of_ssubset.

theorem HasSSubset.SSubset.not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} (h : a ⊂ b) :

Alias of not_subset_of_ssubset.

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

Alias of not_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_of_not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {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} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ⊆ b) (h₂ : b ⊂ c) :

a ⊂ c

theorem ssubset_of_ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ⊂ b) (h₂ : b ⊆ c) :

a ⊂ c

theorem ssubset_of_subset_of_ne {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ⊆ b) (h₂ : a ≠ b) :

a ⊂ b

theorem ssubset_of_ne_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ≠ b) (h₂ : a ⊆ b) :

a ⊂ b

theorem eq_or_ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h : a ⊆ b) :

a = b ∨ a ⊂ b

theorem ssubset_or_eq_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h : a ⊆ b) :

a ⊂ b ∨ a = b

theorem eq_of_subset_of_not_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (hab : a ⊆ b) (hba : ¬a ⊂ b) :

a = b

theorem eq_of_superset_of_not_ssuperset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (hab : a ⊆ b) (hba : ¬a ⊂ b) :

b = a

theorem HasSubset.Subset.trans_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ⊆ b) (h₂ : b ⊂ c) :

a ⊂ c

Alias of ssubset_of_subset_of_ssubset.

theorem HasSSubset.SSubset.trans_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ⊂ b) (h₂ : b ⊆ c) :

a ⊂ c

Alias of ssubset_of_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_of_ne {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ⊆ b) (h₂ : a ≠ b) :

a ⊂ b

Alias of ssubset_of_subset_of_ne.

theorem Ne.ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h₁ : a ≠ b) (h₂ : a ⊆ b) :

a ⊂ b

Alias of ssubset_of_ne_of_subset.

theorem HasSubset.Subset.eq_or_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h : a ⊆ b) :

a = b ∨ a ⊂ b

Alias of eq_or_ssubset_of_subset.

theorem HasSubset.Subset.ssubset_or_eq {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (h : a ⊆ b) :

a ⊂ b ∨ a = b

Alias of ssubset_or_eq_of_subset.

theorem HasSubset.Subset.eq_of_not_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (hab : a ⊆ b) (hba : ¬a ⊂ b) :

a = b

Alias of eq_of_subset_of_not_ssubset.

theorem HasSubset.Subset.eq_of_not_ssuperset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] (hab : a ⊆ b) (hba : ¬a ⊂ b) :

b = a

Alias of eq_of_superset_of_not_ssuperset.

theorem ssubset_iff_subset_ne {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊂ b ↔ a ⊆ b ∧ a ≠ b

theorem subset_iff_ssubset_or_eq {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⊆ x2) fun (x1 x2 : α) => x1 ⊂ x2] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 ⊆ x2] [IsAntisymm α fun (x1 x2 : α) => x1 ⊆ x2] :

a ⊆ b ↔ a ⊂ b ∨ a = b

Conversion of bundled order typeclasses to unbundled relation typeclasses #

instance instIsReflLe {α : Type u} [Preorder α] :

IsRefl α fun (x1 x2 : α) => x1 ≤ x2

instance instIsReflGe {α : Type u} [Preorder α] :

IsRefl α fun (x1 x2 : α) => x1 ≥ x2

instance instIsTransLe {α : Type u} [Preorder α] :

IsTrans α fun (x1 x2 : α) => x1 ≤ x2

instance instIsTransGe {α : Type u} [Preorder α] :

IsTrans α fun (x1 x2 : α) => x1 ≥ x2

instance instIsPreorderLe {α : Type u} [Preorder α] :

IsPreorder α fun (x1 x2 : α) => x1 ≤ x2

instance instIsPreorderGe {α : Type u} [Preorder α] :

IsPreorder α fun (x1 x2 : α) => x1 ≥ x2

instance instIsIrreflLt {α : Type u} [Preorder α] :

IsIrrefl α fun (x1 x2 : α) => x1 < x2

instance instIsIrreflGt {α : Type u} [Preorder α] :

IsIrrefl α fun (x1 x2 : α) => x1 > x2

instance instIsTransLt {α : Type u} [Preorder α] :

IsTrans α fun (x1 x2 : α) => x1 < x2

instance instIsTransGt {α : Type u} [Preorder α] :

IsTrans α fun (x1 x2 : α) => x1 > x2

instance instIsAsymmLt {α : Type u} [Preorder α] :

IsAsymm α fun (x1 x2 : α) => x1 < x2

instance instIsAsymmGt {α : Type u} [Preorder α] :

IsAsymm α fun (x1 x2 : α) => x1 > x2

instance instIsAntisymmLt {α : Type u} [Preorder α] :

IsAntisymm α fun (x1 x2 : α) => x1 < x2

instance instIsAntisymmGt {α : Type u} [Preorder α] :

IsAntisymm α fun (x1 x2 : α) => x1 > x2

instance instIsStrictOrderLt {α : Type u} [Preorder α] :

IsStrictOrder α fun (x1 x2 : α) => x1 < x2

instance instIsStrictOrderGt {α : Type u} [Preorder α] :

IsStrictOrder α fun (x1 x2 : α) => x1 > x2

instance instIsNonstrictStrictOrderLeLt {α : Type u} [Preorder α] :

IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 < x2

instance instIsAntisymmLe {α : Type u} [PartialOrder α] :

IsAntisymm α fun (x1 x2 : α) => x1 ≤ x2

instance instIsAntisymmGe {α : Type u} [PartialOrder α] :

IsAntisymm α fun (x1 x2 : α) => x1 ≥ x2

instance instIsPartialOrderLe {α : Type u} [PartialOrder α] :

IsPartialOrder α fun (x1 x2 : α) => x1 ≤ x2

instance instIsPartialOrderGe {α : Type u} [PartialOrder α] :

IsPartialOrder α fun (x1 x2 : α) => x1 ≥ x2

instance LE.isTotal {α : Type u} [LinearOrder α] :

IsTotal α fun (x1 x2 : α) => x1 ≤ x2

instance instIsTotalGe {α : Type u} [LinearOrder α] :

IsTotal α fun (x1 x2 : α) => x1 ≥ x2

instance instIsLinearOrderLe {α : Type u} [LinearOrder α] :

IsLinearOrder α fun (x1 x2 : α) => x1 ≤ x2

instance instIsLinearOrderGe {α : Type u} [LinearOrder α] :

IsLinearOrder α fun (x1 x2 : α) => x1 ≥ x2

instance instIsTrichotomousLt {α : Type u} [LinearOrder α] :

IsTrichotomous α fun (x1 x2 : α) => x1 < x2

instance instIsTrichotomousGt {α : Type u} [LinearOrder α] :

IsTrichotomous α fun (x1 x2 : α) => x1 > x2

instance instIsTrichotomousLe {α : Type u} [LinearOrder α] :

IsTrichotomous α fun (x1 x2 : α) => x1 ≤ x2

instance instIsTrichotomousGe {α : Type u} [LinearOrder α] :

IsTrichotomous α fun (x1 x2 : α) => x1 ≥ x2

instance instIsStrictTotalOrderLt {α : Type u} [LinearOrder α] :

IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2

instance instIsOrderConnectedLt {α : Type u} [LinearOrder α] :

IsOrderConnected α fun (x1 x2 : α) => x1 < x2

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

Transitive LE.le

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

Transitive LT.lt

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

Transitive GE.ge

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

Transitive GT.gt

instance OrderDual.isTotal_le {α : Type u} [LE α] [h : IsTotal α fun (x1 x2 : α) => x1 ≤ x2] :

IsTotal αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

instance instWellFoundedLTNat :

WellFoundedLT ℕ

@[instance 100]

instance isWellOrder_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] :

IsWellOrder α fun (x1 x2 : α) => x1 < x2

@[instance 100]

instance isWellOrder_gt {α : Type u} [LinearOrder α] [WellFoundedGT α] :

IsWellOrder α fun (x1 x2 : α) => x1 > x2