mathlib3 documentation

order.rel_classes

Unbundled relation classes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_le and/or has_lt while these classes take a relation as an explicit argument.

source
theorem of_eq {α : Type u} {r : α → α → Prop} [is_refl α r] {a b : α} :
a = b → r a b
source
theorem comm {α : Type u} {r : α → α → Prop} [is_symm α r] {a b : α} :
r a b ↔ r b a
source
theorem antisymm' {α : Type u} {r : α → α → Prop} [is_antisymm α r] {a b : α} :
r a b → r b a → b = a
source
theorem antisymm_iff {α : Type u} {r : α → α → Prop} [is_refl α r] [is_antisymm α r] {a b : α} :
r a b ∧ r b a ↔ a = b
source
theorem antisymm_of {α : Type u} (r : α → α → Prop) [is_antisymm α 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.

source
theorem antisymm_of' {α : Type u} (r : α → α → Prop) [is_antisymm α 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.

source
theorem comm_of {α : Type u} (r : α → α → Prop) [is_symm α 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.

source
theorem is_refl.swap {α : Type u} (r : α → α → Prop) [is_refl α r] :
is_refl α (function.swap r)
source
theorem is_irrefl.swap {α : Type u} (r : α → α → Prop) [is_irrefl α r] :
is_irrefl α (function.swap r)
source
theorem is_trans.swap {α : Type u} (r : α → α → Prop) [is_trans α r] :
is_trans α (function.swap r)
source
theorem is_antisymm.swap {α : Type u} (r : α → α → Prop) [is_antisymm α r] :
is_antisymm α (function.swap r)
source
theorem is_asymm.swap {α : Type u} (r : α → α → Prop) [is_asymm α r] :
is_asymm α (function.swap r)
source
theorem is_total.swap {α : Type u} (r : α → α → Prop) [is_total α r] :
is_total α (function.swap r)
source
theorem is_trichotomous.swap {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :
is_trichotomous α (function.swap r)
source
theorem is_preorder.swap {α : Type u} (r : α → α → Prop) [is_preorder α r] :
is_preorder α (function.swap r)
source
theorem is_strict_order.swap {α : Type u} (r : α → α → Prop) [is_strict_order α r] :
is_strict_order α (function.swap r)
source
theorem is_partial_order.swap {α : Type u} (r : α → α → Prop) [is_partial_order α r] :
is_partial_order α (function.swap r)
source
theorem is_total_preorder.swap {α : Type u} (r : α → α → Prop) [is_total_preorder α r] :
is_total_preorder α (function.swap r)
source
theorem is_linear_order.swap {α : Type u} (r : α → α → Prop) [is_linear_order α r] :
is_linear_order α (function.swap r)
source
@[protected]
theorem is_asymm.is_antisymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :
is_antisymm α r
source
@[protected]
theorem is_asymm.is_irrefl {α : Type u} {r : α → α → Prop} [is_asymm α r] :
is_irrefl α r
source
@[protected]
theorem is_total.is_trichotomous {α : Type u} (r : α → α → Prop) [is_total α r] :
is_trichotomous α r
source
@[protected, instance]
def is_total.to_is_refl {α : Type u} (r : α → α → Prop) [is_total α r] :
is_refl α r
source
theorem ne_of_irrefl {α : Type u} {r : α → α → Prop} [is_irrefl α r] {x y : α} :
r x y → x ≠ y
source
theorem ne_of_irrefl' {α : Type u} {r : α → α → Prop} [is_irrefl α r] {x y : α} :
r x y → y ≠ x
source
theorem not_rel_of_subsingleton {α : Type u} (r : α → α → Prop) [is_irrefl α r] [subsingleton α] (x y : α) :
¬r x y
source
theorem rel_of_subsingleton {α : Type u} (r : α → α → Prop) [is_refl α r] [subsingleton α] (x y : α) :
r x y
source
@[simp]
theorem empty_relation_apply {α : Type u} (a b : α) :
empty_relation a b ↔ false
source
theorem eq_empty_relation {α : Type u} (r : α → α → Prop) [is_irrefl α r] [subsingleton α] :
r = empty_relation
source
@[protected, instance]
def empty_relation.is_irrefl {α : Type u} :
is_irrefl α empty_relation
source
theorem trans_trichotomous_left {α : Type u} {r : α → α → Prop} [is_trans α r] [is_trichotomous α r] {a b c : α} :
¬r b a → r b c → r a c
source
theorem trans_trichotomous_right {α : Type u} {r : α → α → Prop} [is_trans α r] [is_trichotomous α r] {a b c : α} :
r a b → ¬r c b → r a c
source
theorem transitive_of_trans {α : Type u} (r : α → α → Prop) [is_trans α r] :
transitive r
source
theorem extensional_of_trichotomous_of_irrefl {α : Type u} (r : α → α → Prop) [is_trichotomous α r] [is_irrefl α 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.

source
@[reducible]
def partial_order_of_SO {α : Type u} (r : α → α → Prop) [is_strict_order α r] :
partial_order α

Construct a partial order from a is_strict_order relation.

See note [reducible non-instances].

Equations
source
@[reducible]
def linear_order_of_STO {α : Type u} (r : α → α → Prop) [is_strict_total_order α r] [Π (x y : α), decidable (¬r x y)] :
linear_order α

Construct a linear order from an is_strict_total_order relation.

See note [reducible non-instances].

Equations
source
theorem is_strict_total_order.swap {α : Type u} (r : α → α → Prop) [is_strict_total_order α r] :
is_strict_total_order α (function.swap r)

Order connection #

source
@[class]
structure is_order_connected (α : Type u) (lt : α → α → Prop) :
Prop
  • 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. 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.

Instances of this typeclass
source
theorem is_order_connected.neg_trans {α : Type u} {r : α → α → Prop} [is_order_connected α r] {a b c : α} (h₁ : ¬r a b) (h₂ : ¬r b c) :
¬r a c
source
theorem is_strict_weak_order_of_is_order_connected {α : Type u} {r : α → α → Prop} [is_asymm α r] [is_order_connected α r] :
is_strict_weak_order α r
source
@[protected, instance]
def is_order_connected_of_is_strict_total_order {α : Type u} {r : α → α → Prop} [is_strict_total_order α r] :
is_order_connected α r
source
@[protected, instance]
def is_strict_weak_order_of_is_strict_total_order {α : Type u} {r : α → α → Prop} [is_strict_total_order α r] :
is_strict_weak_order α r

Well-order #

source
theorem is_well_founded_iff (α : Type u) (r : α → α → Prop) :
is_well_founded α r ↔ well_founded r
source
@[class]
structure is_well_founded (α : Type u) (r : α → α → Prop) :
Prop

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

Instances of this typeclass
source
@[protected, instance]
def has_well_founded.is_well_founded {α : Type u} [h : has_well_founded α] :
is_well_founded α has_well_founded.r
source
theorem is_well_founded.induction {α : Type u} (r : α → α → Prop) [is_well_founded α r] {C : α → Prop} (a : α) :
(∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a

Induction on a well-founded relation.

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

All values are accessible under the well-founded relation.

source
def is_well_founded.fix {α : Type u} (r : α → α → Prop) [is_well_founded α 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 is_well_founded.fix_eq.

Equations
source
theorem is_well_founded.fix_eq {α : Type u} (r : α → α → Prop) [is_well_founded α r] {C : α → Sort u_1} (F : Π (x : α), (Π (y : α), r y x → C y) → C x) (x : α) :
is_well_founded.fix r F x = F x (λ (y : α) (h : r y x), is_well_founded.fix r F y)

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

source
def is_well_founded.to_has_well_founded {α : Type u} (r : α → α → Prop) [is_well_founded α r] :
has_well_founded α

Derive a has_well_founded instance from an is_well_founded instance.

Equations
source
theorem well_founded.asymmetric {α : Sort u_1} {r : α → α → Prop} (h : well_founded r) ⦃a b : α⦄ :
r a b → ¬r b a
source
@[protected, instance]
def is_well_founded.is_asymm {α : Type u} (r : α → α → Prop) [is_well_founded α r] :
is_asymm α r
source
@[protected, instance]
def is_well_founded.is_irrefl {α : Type u} (r : α → α → Prop) [is_well_founded α r] :
is_irrefl α r
source
@[protected, instance]
def relation.trans_gen.is_well_founded {α : Type u} (r : α → α → Prop) [i : is_well_founded α r] :
is_well_founded α (relation.trans_gen r)
source
@[reducible]
def well_founded_lt (α : Type u_1) [has_lt α] :
Prop

A class for a well founded relation <.

Equations
source
@[reducible]
def well_founded_gt (α : Type u_1) [has_lt α] :
Prop

A class for a well founded relation >.

Equations
source
@[protected, instance]
def order_dual.well_founded_gt (α : Type u_1) [has_lt α] [h : well_founded_lt α] :
well_founded_gt αᵒᵈ
source
@[protected, instance]
def order_dual.well_founded_lt (α : Type u_1) [has_lt α] [h : well_founded_gt α] :
well_founded_lt αᵒᵈ
source
theorem well_founded_gt_dual_iff (α : Type u_1) [has_lt α] :
well_founded_gt αᵒᵈ ↔ well_founded_lt α
source
theorem well_founded_lt_dual_iff (α : Type u_1) [has_lt α] :
well_founded_lt αᵒᵈ ↔ well_founded_gt α
source
@[class]
structure is_well_order (α : Type u) (r : α → α → Prop) :
Prop

A well order is a well-founded linear order.

Instances of this typeclass
source
@[protected, instance]
def is_well_order.is_strict_total_order {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
is_strict_total_order α r
source
@[protected, instance]
def is_well_order.is_trichotomous {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
is_trichotomous α r
source
@[protected, instance]
def is_well_order.is_trans {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
is_trans α r
source
@[protected, instance]
def is_well_order.is_irrefl {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
is_irrefl α r
source
@[protected, instance]
def is_well_order.is_asymm {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
is_asymm α r
source
theorem well_founded_lt.induction {α : Type u} [has_lt α] [well_founded_lt α] {C : α → Prop} (a : α) :
(∀ (x : α), (∀ (y : α), y < x → C y) → C x) → C a

Inducts on a well-founded < relation.

source
theorem well_founded_lt.apply {α : Type u} [has_lt α] [well_founded_lt α] (a : α) :
acc has_lt.lt a

All values are accessible under the well-founded <.

source
def well_founded_lt.fix {α : Type u} [has_lt α] [well_founded_lt α] {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 well_founded_lt.fix_eq.

Equations
source
theorem well_founded_lt.fix_eq {α : Type u} [has_lt α] [well_founded_lt α] {C : α → Sort u_1} (F : Π (x : α), (Π (y : α), y < x → C y) → C x) (x : α) :
well_founded_lt.fix F x = F x (λ (y : α) (h : y < x), well_founded_lt.fix F y)

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

source
def well_founded_lt.to_has_well_founded {α : Type u} [has_lt α] [well_founded_lt α] :
has_well_founded α

Derive a has_well_founded instance from a well_founded_lt instance.

Equations
source
theorem well_founded_gt.induction {α : Type u} [has_lt α] [well_founded_gt α] {C : α → Prop} (a : α) :
(∀ (x : α), (∀ (y : α), x < y → C y) → C x) → C a

Inducts on a well-founded > relation.

source
theorem well_founded_gt.apply {α : Type u} [has_lt α] [well_founded_gt α] (a : α) :
acc gt a

All values are accessible under the well-founded >.

source
def well_founded_gt.fix {α : Type u} [has_lt α] [well_founded_gt α] {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 well_founded_gt.fix_eq.

Equations
source
theorem well_founded_gt.fix_eq {α : Type u} [has_lt α] [well_founded_gt α] {C : α → Sort u_1} (F : Π (x : α), (Π (y : α), x < y → C y) → C x) (x : α) :
well_founded_gt.fix F x = F x (λ (y : α) (h : x < y), well_founded_gt.fix F y)

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

source
def well_founded_gt.to_has_well_founded {α : Type u} [has_lt α] [well_founded_gt α] :
has_well_founded α

Derive a has_well_founded instance from a well_founded_gt instance.

Equations
source
noncomputable def is_well_order.linear_order {α : Type u} (r : α → α → Prop) [is_well_order α r] :
linear_order α

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

Equations
source
def is_well_order.to_has_well_founded {α : Type u} [has_lt α] [hwo : is_well_order α has_lt.lt] :
has_well_founded α

Derive a has_well_founded instance from a is_well_order instance.

Equations
source
theorem subsingleton.is_well_order {α : Type u} [subsingleton α] (r : α → α → Prop) [hr : is_irrefl α r] :
is_well_order α r
source
@[protected, instance]
def empty_relation.is_well_order {α : Type u} [subsingleton α] :
is_well_order α empty_relation
source
@[protected, instance]
def is_empty.is_well_order {α : Type u} [is_empty α] (r : α → α → Prop) :
is_well_order α r
source
@[protected, instance]
def prod.lex.is_well_founded {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_founded α r] [is_well_founded β s] :
is_well_founded (α × β) (prod.lex r s)
source
@[protected, instance]
def prod.lex.is_well_order {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
is_well_order (α × β) (prod.lex r s)
source
@[protected, instance]
def inv_image.is_well_founded {α : Type u} {β : Type v} (r : α → α → Prop) [is_well_founded α r] (f : β → α) :
is_well_founded β (inv_image r f)
source
@[protected, instance]
def measure.is_well_founded {α : Type u} (f : α → ℕ) :
is_well_founded α (measure f)
source
theorem subrelation.is_well_founded {α : Type u} (r : α → α → Prop) [is_well_founded α r] {s : α → α → Prop} (h : subrelation s r) :
is_well_founded α s
source
def set.unbounded {α : Type u} (r : α → α → Prop) (s : set α) :
Prop

An unbounded or cofinal set.

Equations
source
def set.bounded {α : Type u} (r : α → α → Prop) (s : set α) :
Prop

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

Equations
source
@[simp]
theorem set.not_bounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :
¬set.bounded r s ↔ set.unbounded r s
source
@[simp]
theorem set.not_unbounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :
¬set.unbounded r s ↔ set.bounded r s
source
theorem set.unbounded_of_is_empty {α : Type u} [is_empty α] {r : α → α → Prop} (s : set α) :
set.unbounded r s
source
@[protected, instance]
def prod.is_refl_preimage_fst {α : Type u} {r : α → α → Prop} [h : is_refl α r] :
is_refl (α × α) (prod.fst ⁻¹'o r)
source
@[protected, instance]
def prod.is_refl_preimage_snd {α : Type u} {r : α → α → Prop} [h : is_refl α r] :
is_refl (α × α) (prod.snd ⁻¹'o r)
source
@[protected, instance]
def prod.is_trans_preimage_fst {α : Type u} {r : α → α → Prop} [h : is_trans α r] :
is_trans (α × α) (prod.fst ⁻¹'o r)
source
@[protected, instance]
def prod.is_trans_preimage_snd {α : Type u} {r : α → α → Prop} [h : is_trans α r] :
is_trans (α × α) (prod.snd ⁻¹'o r)

Strict-non strict relations #

source
@[class]
structure is_nonstrict_strict_order (α : Type u_1) (r s : α → α → Prop) :
Type
  • 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 of this typeclass
Instances of other typeclasses for is_nonstrict_strict_order
  • is_nonstrict_strict_order.has_sizeof_inst
source
theorem right_iff_left_not_left {α : Type u} {r s : α → α → Prop} [is_nonstrict_strict_order α r s] {a b : α} :
s a b ↔ r a b ∧ ¬r b a
source
theorem right_iff_left_not_left_of {α : Type u} (r s : α → α → Prop) [is_nonstrict_strict_order α 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.

source
@[protected, nolint, instance]
def is_nonstrict_strict_order.to_is_irrefl {α : Type u} {r s : α → α → Prop} [is_nonstrict_strict_order α r s] :
is_irrefl α s

⊆ and ⊂ #

source
theorem subset_of_eq_of_subset {α : Type u} [has_subset α] {a b c : α} (hab : a = b) (hbc : b ⊆ c) :
a ⊆ c
source
theorem subset_of_subset_of_eq {α : Type u} [has_subset α] {a b c : α} (hab : a ⊆ b) (hbc : b = c) :
a ⊆ c
source
@[refl]
theorem subset_refl {α : Type u} [has_subset α] [is_refl α has_subset.subset] (a : α) :
a ⊆ a
source
theorem subset_rfl {α : Type u} [has_subset α] {a : α} [is_refl α has_subset.subset] :
a ⊆ a
source
theorem subset_of_eq {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = b → a ⊆ b
source
theorem superset_of_eq {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = b → b ⊆ a
source
theorem ne_of_not_subset {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
¬a ⊆ b → a ≠ b
source
theorem ne_of_not_superset {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
¬a ⊆ b → b ≠ a
source
@[trans]
theorem subset_trans {α : Type u} [has_subset α] [is_trans α has_subset.subset] {a b c : α} :
a ⊆ b → b ⊆ c → a ⊆ c
source
theorem subset_antisymm {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) (h' : b ⊆ a) :
a = b
source
theorem superset_antisymm {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) (h' : b ⊆ a) :
b = a
source
theorem eq.trans_subset {α : Type u} [has_subset α] {a b c : α} (hab : a = b) (hbc : b ⊆ c) :
a ⊆ c

Alias of subset_of_eq_of_subset.

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

Alias of subset_of_subset_of_eq.

source
theorem eq.subset' {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = b → a ⊆ b

Alias of subset_of_eq.

source
theorem eq.superset {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = b → b ⊆ a

Alias of superset_of_eq.

source
theorem has_subset.subset.trans {α : Type u} [has_subset α] [is_trans α has_subset.subset] {a b c : α} :
a ⊆ b → b ⊆ c → a ⊆ c

Alias of subset_trans.

source
theorem has_subset.subset.antisymm {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) (h' : b ⊆ a) :
a = b

Alias of subset_antisymm.

source
theorem has_subset.subset.antisymm' {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) (h' : b ⊆ a) :
b = a

Alias of superset_antisymm.

source
theorem subset_antisymm_iff {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] [is_antisymm α has_subset.subset] :
a = b ↔ a ⊆ b ∧ b ⊆ a
source
theorem superset_antisymm_iff {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] [is_antisymm α has_subset.subset] :
a = b ↔ b ⊆ a ∧ a ⊆ b
source
theorem ssubset_of_eq_of_ssubset {α : Type u} [has_ssubset α] {a b c : α} (hab : a = b) (hbc : b ⊂ c) :
a ⊂ c
source
theorem ssubset_of_ssubset_of_eq {α : Type u} [has_ssubset α] {a b c : α} (hab : a ⊂ b) (hbc : b = c) :
a ⊂ c
source
theorem ssubset_irrefl {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] (a : α) :
¬a ⊂ a
source
theorem ssubset_irrfl {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a : α} :
¬a ⊂ a
source
theorem ne_of_ssubset {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a ⊂ b → a ≠ b
source
theorem ne_of_ssuperset {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a ⊂ b → b ≠ a
source
@[trans]
theorem ssubset_trans {α : Type u} [has_ssubset α] [is_trans α has_ssubset.ssubset] {a b c : α} :
a ⊂ b → b ⊂ c → a ⊂ c
source
theorem ssubset_asymm {α : Type u} [has_ssubset α] [is_asymm α has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
¬b ⊂ a
source
theorem eq.trans_ssubset {α : Type u} [has_ssubset α] {a b c : α} (hab : a = b) (hbc : b ⊂ c) :
a ⊂ c

Alias of ssubset_of_eq_of_ssubset.

source
theorem has_ssubset.ssubset.trans_eq {α : Type u} [has_ssubset α] {a b c : α} (hab : a ⊂ b) (hbc : b = c) :
a ⊂ c

Alias of ssubset_of_ssubset_of_eq.

source
theorem has_ssubset.ssubset.false {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a : α} :
¬a ⊂ a

Alias of ssubset_irrfl.

source
theorem has_ssubset.ssubset.ne {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a ⊂ b → a ≠ b

Alias of ne_of_ssubset.

source
theorem has_ssubset.ssubset.ne' {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a ⊂ b → b ≠ a

Alias of ne_of_ssuperset.

source
theorem has_ssubset.ssubset.trans {α : Type u} [has_ssubset α] [is_trans α has_ssubset.ssubset] {a b c : α} :
a ⊂ b → b ⊂ c → a ⊂ c

Alias of ssubset_trans.

source
theorem has_ssubset.ssubset.asymm {α : Type u} [has_ssubset α] [is_asymm α has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
¬b ⊂ a

Alias of ssubset_asymm.

source
theorem ssubset_iff_subset_not_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} :
a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a
source
theorem subset_of_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
a ⊆ b
source
theorem not_subset_of_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
¬b ⊆ a
source
theorem not_ssubset_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a ⊆ b) :
¬b ⊂ a
source
theorem ssubset_of_subset_not_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h₁ : a ⊆ b) (h₂ : ¬b ⊆ a) :
a ⊂ b
source
theorem has_ssubset.ssubset.subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
a ⊆ b

Alias of subset_of_ssubset.

source
theorem has_ssubset.ssubset.not_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a ⊂ b) :
¬b ⊆ a

Alias of not_subset_of_ssubset.

source
theorem has_subset.subset.not_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a ⊆ b) :
¬b ⊂ a

Alias of not_ssubset_of_subset.

source
theorem has_subset.subset.ssubset_of_not_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h₁ : a ⊆ b) (h₂ : ¬b ⊆ a) :
a ⊂ b

Alias of ssubset_of_subset_not_subset.

source
theorem ssubset_of_subset_of_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b c : α} [is_trans α has_subset.subset] (h₁ : a ⊆ b) (h₂ : b ⊂ c) :
a ⊂ c
source
theorem ssubset_of_ssubset_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b c : α} [is_trans α has_subset.subset] (h₁ : a ⊂ b) (h₂ : b ⊆ c) :
a ⊂ c
source
theorem ssubset_of_subset_of_ne {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h₁ : a ⊆ b) (h₂ : a ≠ b) :
a ⊂ b
source
theorem ssubset_of_ne_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h₁ : a ≠ b) (h₂ : a ⊆ b) :
a ⊂ b
source
theorem eq_or_ssubset_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) :
a = b ∨ a ⊂ b
source
theorem ssubset_or_eq_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) :
a ⊂ b ∨ a = b
source
theorem has_subset.subset.trans_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b c : α} [is_trans α has_subset.subset] (h₁ : a ⊆ b) (h₂ : b ⊂ c) :
a ⊂ c

Alias of ssubset_of_subset_of_ssubset.

source
theorem has_ssubset.ssubset.trans_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b c : α} [is_trans α has_subset.subset] (h₁ : a ⊂ b) (h₂ : b ⊆ c) :
a ⊂ c

Alias of ssubset_of_ssubset_of_subset.

source
theorem has_subset.subset.ssubset_of_ne {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h₁ : a ⊆ b) (h₂ : a ≠ b) :
a ⊂ b

Alias of ssubset_of_subset_of_ne.

source
theorem ne.ssubset_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h₁ : a ≠ b) (h₂ : a ⊆ b) :
a ⊂ b

Alias of ssubset_of_ne_of_subset.

source
theorem has_subset.subset.eq_or_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) :
a = b ∨ a ⊂ b

Alias of eq_or_ssubset_of_subset.

source
theorem has_subset.subset.ssubset_or_eq {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h : a ⊆ b) :
a ⊂ b ∨ a = b

Alias of ssubset_or_eq_of_subset.

source
theorem ssubset_iff_subset_ne {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] :
a ⊂ b ↔ a ⊆ b ∧ a ≠ b
source
theorem subset_iff_ssubset_or_eq {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_refl α has_subset.subset] [is_antisymm α has_subset.subset] :
a ⊆ b ↔ a ⊂ b ∨ a = b

Conversion of bundled order typeclasses to unbundled relation typeclasses #

source
@[protected, instance]
def has_le.le.is_refl {α : Type u} [preorder α] :
is_refl α has_le.le
source
@[protected, instance]
def ge.is_refl {α : Type u} [preorder α] :
is_refl α ge
source
@[protected, instance]
def has_le.le.is_trans {α : Type u} [preorder α] :
is_trans α has_le.le
source
@[protected, instance]
def ge.is_trans {α : Type u} [preorder α] :
is_trans α ge
source
@[protected, instance]
def has_le.le.is_preorder {α : Type u} [preorder α] :
is_preorder α has_le.le
source
@[protected, instance]
def ge.is_preorder {α : Type u} [preorder α] :
is_preorder α ge
source
@[protected, instance]
def has_lt.lt.is_irrefl {α : Type u} [preorder α] :
is_irrefl α has_lt.lt
source
@[protected, instance]
def gt.is_irrefl {α : Type u} [preorder α] :
is_irrefl α gt
source
@[protected, instance]
def has_lt.lt.is_trans {α : Type u} [preorder α] :
is_trans α has_lt.lt
source
@[protected, instance]
def gt.is_trans {α : Type u} [preorder α] :
is_trans α gt
source
@[protected, instance]
def has_lt.lt.is_asymm {α : Type u} [preorder α] :
is_asymm α has_lt.lt
source
@[protected, instance]
def gt.is_asymm {α : Type u} [preorder α] :
is_asymm α gt
source
@[protected, instance]
def has_lt.lt.is_antisymm {α : Type u} [preorder α] :
is_antisymm α has_lt.lt
source
@[protected, instance]
def gt.is_antisymm {α : Type u} [preorder α] :
is_antisymm α gt
source
@[protected, instance]
def has_lt.lt.is_strict_order {α : Type u} [preorder α] :
is_strict_order α has_lt.lt
source
@[protected, instance]
def gt.is_strict_order {α : Type u} [preorder α] :
is_strict_order α gt
source
@[protected, instance]
def has_lt.lt.is_nonstrict_strict_order {α : Type u} [preorder α] :
is_nonstrict_strict_order α has_le.le has_lt.lt
Equations
source
@[protected, instance]
def has_le.le.is_antisymm {α : Type u} [partial_order α] :
is_antisymm α has_le.le
source
@[protected, instance]
def ge.is_antisymm {α : Type u} [partial_order α] :
is_antisymm α ge
source
@[protected, instance]
def has_le.le.is_partial_order {α : Type u} [partial_order α] :
is_partial_order α has_le.le
source
@[protected, instance]
def ge.is_partial_order {α : Type u} [partial_order α] :
is_partial_order α ge
source
@[protected, instance]
def has_le.le.is_total {α : Type u} [linear_order α] :
is_total α has_le.le
source
@[protected, instance]
def ge.is_total {α : Type u} [linear_order α] :
is_total α ge
source
@[protected, instance]
def linear_order.is_total_preorder {α : Type u} [linear_order α] :
is_total_preorder α has_le.le
source
@[protected, instance]
def ge.is_total_preorder {α : Type u} [linear_order α] :
is_total_preorder α ge
source
@[protected, instance]
def has_le.le.is_linear_order {α : Type u} [linear_order α] :
is_linear_order α has_le.le
source
@[protected, instance]
def ge.is_linear_order {α : Type u} [linear_order α] :
is_linear_order α ge
source
@[protected, instance]
def has_lt.lt.is_trichotomous {α : Type u} [linear_order α] :
is_trichotomous α has_lt.lt
source
@[protected, instance]
def gt.is_trichotomous {α : Type u} [linear_order α] :
is_trichotomous α gt
source
@[protected, instance]
def has_le.le.is_trichotomous {α : Type u} [linear_order α] :
is_trichotomous α has_le.le
source
@[protected, instance]
def ge.is_trichotomous {α : Type u} [linear_order α] :
is_trichotomous α ge
source
@[protected, instance]
def has_lt.lt.is_strict_total_order {α : Type u} [linear_order α] :
is_strict_total_order α has_lt.lt
source
@[protected, instance]
def has_lt.lt.is_order_connected {α : Type u} [linear_order α] :
is_order_connected α has_lt.lt
source
@[protected, instance]
def has_lt.lt.is_incomp_trans {α : Type u} [linear_order α] :
is_incomp_trans α has_lt.lt
source
@[protected, instance]
def has_lt.lt.is_strict_weak_order {α : Type u} [linear_order α] :
is_strict_weak_order α has_lt.lt
source
theorem transitive_le {α : Type u} [preorder α] :
transitive has_le.le
source
theorem transitive_lt {α : Type u} [preorder α] :
transitive has_lt.lt
source
theorem transitive_ge {α : Type u} [preorder α] :
transitive ge
source
theorem transitive_gt {α : Type u} [preorder α] :
transitive gt
source
@[protected, instance]
def order_dual.is_total_le {α : Type u} [has_le α] [is_total α has_le.le] :
is_total αᵒᵈ has_le.le
source
@[protected, instance]
def nat.well_founded_lt  :
well_founded_lt ℕ
source
@[protected, instance]
def nat.lt.is_well_order  :
is_well_order ℕ has_lt.lt
source
@[protected, instance]
def gt.is_well_order {α : Type u} [linear_order α] [h : is_well_order α has_lt.lt] :
is_well_order αᵒᵈ gt
source
@[protected, instance]
def has_lt.lt.is_well_order {α : Type u} [linear_order α] [h : is_well_order α gt] :
is_well_order αᵒᵈ has_lt.lt