mathlib documentation

core / init.algebra.classes

Unbundled algebra classes #

These classes and the @[algebra] attribute are part of an incomplete refactor described here on the github Wiki.

By themselves, these classes are not good replacements for the monoid / group etc structures provided by mathlib, as they are not discoverable by simp unlike the current lemmas due to there being little to index on. The Wiki page linked above describes an algebraic normalizer, but it is not implemented.

@[class]

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

Prop

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

Instances of this typeclass

@[class]

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

Prop

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

Instances of this typeclass

@[protected, 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 of this typeclass

@[class]

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

Prop

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

Instances of this typeclass

@[class]

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

Prop

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

Instances of this typeclass

@[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 of this typeclass

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 of this typeclass

equiv.arrow_congr.is_right_cancel

@[class]

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

Prop

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

Instances of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[protected, 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 of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[protected, 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 of this typeclass

@[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 of this typeclass

@[class]

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

Prop

to_is_preorder : is_preorder α r
to_is_symm : is_symm α r

Instances of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[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 of this typeclass

@[class]

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

Prop

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

Instances of this typeclass

@[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 of this typeclass

@[protected, 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

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

Instances for strict_weak_order.equiv

strict_weak_order.is_equiv

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

@[protected, 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