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

@[class]

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

Prop

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

Instances

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

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

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

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

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

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

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

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