mathlib documentation

core / init.algebra.classes

@[class]

structure is_symm_op (α : Type u) (β : out_param (Type v)) (op : α → α → β) :

Prop

symm_op : ∀ (a b : α), op a b = op b a

Instances

@[class]

structure is_commutative (α : Type u) (op : α → α → α) :

Prop

comm : ∀ (a b : α), op a b = op b a

Instances

@[instance]

def is_symm_op_of_is_commutative (α : Type u) (op : α → α → α) [is_commutative α op] :

is_symm_op α α op

@[class]

structure is_associative (α : Type u) (op : α → α → α) :

Prop

assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)

Instances

@[class]

structure is_left_id (α : Type u) (op : α → α → α) (o : out_param α) :

Prop

left_id : ∀ (a : α), op o a = a

Instances

@[class]

structure is_right_id (α : Type u) (op : α → α → α) (o : out_param α) :

Prop

right_id : ∀ (a : α), op a o = a

Instances

@[class]

structure is_left_null (α : Type u) (op : α → α → α) (o : out_param α) :

Prop

left_null : ∀ (a : α), op o a = o

@[class]

structure is_right_null (α : Type u) (op : α → α → α) (o : out_param α) :

Prop

right_null : ∀ (a : α), op a o = o

@[class]

structure is_left_cancel (α : Type u) (op : α → α → α) :

Prop

left_cancel : ∀ (a b c : α), op a b = op a c → b = c

Instances

equiv.arrow_congr.is_left_cancel

@[class]

structure is_right_cancel (α : Type u) (op : α → α → α) :

Prop

right_cancel : ∀ (a b c : α), op a b = op c b → a = c

Instances

equiv.arrow_congr.is_right_cancel

@[class]

structure is_idempotent (α : Type u) (op : α → α → α) :

Prop

idempotent : ∀ (a : α), op a a = a

Instances

@[class]

structure is_left_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param (α → α → α)) :

Prop

left_distrib : ∀ (a b c : α), op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c)

@[class]

structure is_right_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param (α → α → α)) :

Prop

right_distrib : ∀ (a b c : α), op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c)

@[class]

structure is_left_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) :

Prop

left_inv : ∀ (a : α), op (inv a) a = o

@[class]

structure is_right_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) :

Prop

right_inv : ∀ (a : α), op a (inv a) = o

@[class]

structure is_cond_left_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) (p : out_param (α → Prop)) :

Prop

left_inv : ∀ (a : α), p a → op (inv a) a = o

@[class]

structure is_cond_right_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) (p : out_param (α → Prop)) :

Prop

right_inv : ∀ (a : α), p a → op a (inv a) = o

@[class]

structure is_distinct (α : Type u) (a b : α) :

Prop

distinct : a ≠ b

@[class]

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

Prop

irrefl : ∀ (a : α), ¬r a a

is_irrefl X r means the binary relation r on X is irreflexive (that is, r x x never holds).

Instances

@[class]

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

Prop

refl : ∀ (a : α), r a a

is_refl X r means the binary relation r on X is reflexive.

Instances

@[class]

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

Prop

symm : ∀ (a b : α), r a b → r b a

is_symm X r means the binary relation r on X is symmetric.

Instances

@[instance]

def is_symm_op_of_is_symm (α : Type u) (r : α → α → Prop) [is_symm α r] :

is_symm_op α Prop r

The opposite of a symmetric relation is symmetric.

@[class]

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

Prop

asymm : ∀ (a b : α), r a b → ¬r b a

is_asymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

Instances

@[class]

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

Prop

antisymm : ∀ (a b : α), r a b → r b a → a = b

is_antisymm X r means the binary relation r on X is antisymmetric.

Instances

@[class]

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

Prop

trans : ∀ (a b c : α), r a b → r b c → r a c

is_trans X r means the binary relation r on X is transitive.

Instances

@[class]

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

Prop

total : ∀ (a b : α), r a b ∨ r b a

is_total X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

Instances

@[class]

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

Prop

to_is_refl : is_refl α r
to_is_trans : is_trans α r

is_preorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

Instances

@[class]

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

Prop

to_is_trans : is_trans α r
to_is_total : is_total α r

is_total_preorder X r means that the binary relation r on X is total and a preorder.

Instances

@[instance]

def is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] :

is_preorder α r

Every total pre-order is a pre-order.

@[class]

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

Prop

to_is_preorder : is_preorder α r
to_is_antisymm : is_antisymm α r

Instances

@[class]

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

Prop

to_is_partial_order : is_partial_order α r
to_is_total : is_total α r

Instances

@[class]

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

Prop

to_is_preorder : is_preorder α r
to_is_symm : is_symm α r

Instances

@[class]

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

Prop

to_is_symm : is_symm α r
to_is_trans : is_trans α r

@[class]

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

Prop

to_is_irrefl : is_irrefl α r
to_is_trans : is_trans α r

Instances

@[class]

structure is_incomp_trans (α : Type u) (lt : α → α → Prop) :

Prop

incomp_trans : ∀ (a b c : α), ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

Instances

@[class]

structure is_strict_weak_order (α : Type u) (lt : α → α → Prop) :

Prop

to_is_strict_order : is_strict_order α lt
to_is_incomp_trans : is_incomp_trans α lt

Instances

@[class]

structure is_trichotomous (α : Type u) (lt : α → α → Prop) :

Prop

trichotomous : ∀ (a b : α), lt a b ∨ a = b ∨ lt b a

Instances

@[class]

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

Prop

to_is_trichotomous : is_trichotomous α lt
to_is_strict_weak_order : is_strict_weak_order α lt

Instances

@[instance]

def eq_is_equiv (α : Type u) :

theorem irrefl {α : Type u} {r : α → α → Prop} [is_irrefl α r] (a : α) :

¬r a a

theorem refl {α : Type u} {r : α → α → Prop} [is_refl α r] (a : α) :

r a a

theorem trans {α : Type u} {r : α → α → Prop} [is_trans α r] {a b c : α} :

r a b → r b c → r a c

theorem symm {α : Type u} {r : α → α → Prop} [is_symm α r] {a b : α} :

r a b → r b a

theorem antisymm {α : Type u} {r : α → α → Prop} [is_antisymm α r] {a b : α} :

r a b → r b a → a = b

theorem asymm {α : Type u} {r : α → α → Prop} [is_asymm α r] {a b : α} :

r a b → ¬r b a

theorem trichotomous {α : Type u} {r : α → α → Prop} [is_trichotomous α r] (a b : α) :

r a b ∨ a = b ∨ r b a

theorem incomp_trans {α : Type u} {r : α → α → Prop} [is_incomp_trans α r] {a b c : α} :

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

@[instance]

def is_asymm_of_is_trans_of_is_irrefl {α : Type u} {r : α → α → Prop} [is_trans α r] [is_irrefl α r] :

theorem irrefl_of {α : Type u} (r : α → α → Prop) [is_irrefl α r] (a : α) :

¬r a a

theorem refl_of {α : Type u} (r : α → α → Prop) [is_refl α r] (a : α) :

r a a

theorem trans_of {α : Type u} (r : α → α → Prop) [is_trans α r] {a b c : α} :

r a b → r b c → r a c

theorem symm_of {α : Type u} (r : α → α → Prop) [is_symm α r] {a b : α} :

r a b → r b a

theorem asymm_of {α : Type u} (r : α → α → Prop) [is_asymm α r] {a b : α} :

r a b → ¬r b a

theorem total_of {α : Type u} (r : α → α → Prop) [is_total α r] (a b : α) :

r a b ∨ r b a

theorem trichotomous_of {α : Type u} (r : α → α → Prop) [is_trichotomous α r] (a b : α) :

r a b ∨ a = b ∨ r b a

theorem incomp_trans_of {α : Type u} (r : α → α → Prop) [is_incomp_trans α r] {a b c : α} :

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

def strict_weak_order.equiv {α : Type u} {r : α → α → Prop} (a b : α) :

Prop

Equations

strict_weak_order.equiv a b = (¬r a b ∧ ¬r b a)

theorem strict_weak_order.erefl {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] (a : α) :

strict_weak_order.equiv a a

theorem strict_weak_order.esymm {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b : α} :

strict_weak_order.equiv a b → strict_weak_order.equiv b a

theorem strict_weak_order.etrans {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b c : α} :

strict_weak_order.equiv a b → strict_weak_order.equiv b c → strict_weak_order.equiv a c

theorem strict_weak_order.not_lt_of_equiv {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b : α} :

strict_weak_order.equiv a b → ¬r a b

theorem strict_weak_order.not_lt_of_equiv' {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] {a b : α} :

strict_weak_order.equiv a b → ¬r b a

@[instance]

def strict_weak_order.is_equiv {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] :

is_equiv α strict_weak_order.equiv

theorem is_strict_weak_order_of_is_total_preorder {α : Type u} {le lt : α → α → Prop} [decidable_rel le] [s : is_total_preorder α le] (h : ∀ (a b : α), lt a b ↔ ¬le b a) :

is_strict_weak_order α lt

theorem lt_of_lt_of_incomp {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] [decidable_rel lt] {a b c : α} :

lt a b → ¬lt b c ∧ ¬lt c b → lt a c

theorem lt_of_incomp_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] [decidable_rel lt] {a b c : α} :

¬lt a b ∧ ¬lt b a → lt b c → lt a c

theorem eq_of_incomp {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b : α} :

¬lt a b ∧ ¬lt b a → a = b

theorem eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b : α} :

strict_weak_order.equiv a b → a = b

theorem incomp_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b : α) :

¬lt a b ∧ ¬lt b a ↔ a = b

theorem eqv_lt_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b : α) :

strict_weak_order.equiv a b ↔ a = b

theorem not_lt_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_order α lt] {a b : α} :

lt a b → ¬lt b a