order.rel_classes - mathlib docs

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 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

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

partial_order_of_SO r = {le := λ (x y : α), x = y ∨ r x y, lt := r, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[class]

structure is_strict_total_order' (α : Type u) (lt : α → α → Prop) :

Prop

to_is_trichotomous : is_trichotomous α lt
to_is_strict_order : is_strict_order α lt

This is basically the same as is_strict_total_order, but that definition has a redundant assumption is_incomp_trans α lt.

Instances

source

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

linear_order_of_STO' r = {le := partial_order.le (partial_order_of_SO r), lt := partial_order.lt (partial_order_of_SO r), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (x y : α), decidable_of_iff (¬r y x) _, decidable_eq := decidable_eq_of_decidable_le (λ (x y : α), decidable_of_iff (¬r y x) _), decidable_lt := decidable_lt_of_decidable_le (λ (x y : α), decidable_of_iff (¬r y x) _), max := max_default (λ (a b : α), decidable_of_iff (¬r b a) _), max_def := _, min := min_default (λ (a b : α), decidable_of_iff (¬r b a) _), min_def := _}

source

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

is_strict_total_order' α (function.swap r)

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

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_total_order_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

is_strict_total_order α r

source

@[class]

structure is_extensional (α : Type u) (r : α → α → Prop) :

Prop

ext : ∀ (a b : α), (∀ (x : α), r x a ↔ r x b) → a = b

An extensional relation is one in which an element is determined by its set of predecessors. It is named for the x ∈ y relation in set theory, whose extensionality is one of the first axioms of ZFC.

Instances

source

@[protected, instance]

def is_extensional_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

is_extensional α r

source

@[class]

structure is_well_order (α : Type u) (r : α → α → Prop) :

Prop

to_is_strict_total_order' : is_strict_total_order' α r
wf : well_founded r

A well order is a well-founded linear order.

Instances

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_extensional {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

is_extensional α 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

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

is_well_order.linear_order r = let _inst : Π (x y : α), decidable (¬r x y) := λ (x y : α), classical.dec (¬r x y) in linear_order_of_STO' r

source

@[protected, instance]

def empty_relation.is_well_order {α : Type u} [subsingleton α] :

is_well_order α empty_relation

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

def set.unbounded {α : Type u} (r : α → α → Prop) (s : set α) :

Prop

An unbounded or cofinal set.

Equations

set.unbounded r s = ∀ (a : α), ∃ (b : α) (H : b ∈ s), ¬r b a

source

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

Prop

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

Equations

set.bounded r s = ∃ (a : α), ∀ (b : α), b ∈ s → r b a

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

@[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)

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

source