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

source
@[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
source
@[class]
structure is_commutative (α : Type u) (op : α → α → α) :
Prop
  • comm : ∀ (a b : α), op a b = op b a
Instances of this typeclass
source
@[protected, instance]
def is_symm_op_of_is_commutative (α : Type u) (op : α → α → α) [is_commutative α op] :
is_symm_op α α op
source
@[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
source
@[class]
structure is_left_id (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • left_id : ∀ (a : α), op o a = a
Instances of this typeclass
source
@[class]
structure is_right_id (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • right_id : ∀ (a : α), op a o = a
Instances of this typeclass
source
@[class]
structure is_left_null (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • left_null : ∀ (a : α), op o a = o
source
@[class]
structure is_right_null (α : Type u) (op : α → α → α) (o : out_param α) :
Prop
  • right_null : ∀ (a : α), op a o = o
source
@[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
source
@[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
source
@[class]
structure is_idempotent (α : Type u) (op : α → α → α) :
Prop
  • idempotent : ∀ (a : α), op a a = a
Instances of this typeclass
source
@[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)
source
@[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)
source
@[class]
structure is_left_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) :
Prop
  • left_inv : ∀ (a : α), op (inv a) a = o
source
@[class]
structure is_right_inv (α : Type u) (op : α → α → α) (inv : out_param (α → α)) (o : out_param α) :
Prop
  • right_inv : ∀ (a : α), op a (inv a) = o
source
@[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
source
@[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
source
@[class]
structure is_distinct (α : Type u) (a b : α) :
Prop
  • distinct : a ≠ b
source
@[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
source
@[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
source
@[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
source
@[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.

source
@[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
source
@[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
source
@[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
source
@[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
source
@[class]
structure is_preorder (α : Type u) (r : α → α → Prop) :
Prop

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
source
@[class]
structure is_total_preorder (α : Type u) (r : α → α → Prop) :
Prop

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

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

source
@[class]
structure is_partial_order (α : Type u) (r : α → α → Prop) :
Prop

is_partial_order X r means that the binary relation r on X is a partial order, that is, is_preorder X r and is_antisymm X r.

Instances of this typeclass
source
@[class]
structure is_linear_order (α : Type u) (r : α → α → Prop) :
Prop

is_linear_order X r means that the binary relation r on X is a linear order, that is, is_partial_order X r and is_total X r.

Instances of this typeclass
source
@[class]
structure is_equiv (α : Type u) (r : α → α → Prop) :
Prop

is_equiv X r means that the binary relation r on X is an equivalence relation, that is, is_preorder X r and is_symm X r.

Instances of this typeclass
source
@[class]
structure is_per (α : Type u) (r : α → α → Prop) :
Prop

is_per X r means that the binary relation r on X is a partial equivalence relation, that is, is_symm X r and is_trans X r.

source
@[class]
structure is_strict_order (α : Type u) (r : α → α → Prop) :
Prop

is_strict_order X r means that the binary relation r on X is a strict order, that is, is_irrefl X r and is_trans X r.

Instances of this typeclass
source
@[class]
structure is_incomp_trans (α : Type u) (lt : α → α → Prop) :
Prop

is_incomp_trans X lt means that for lt a binary relation on X, the incomparable relation λ a b, ¬ lt a b ∧ ¬ lt b a is transitive.

Instances of this typeclass
source
@[class]
structure is_strict_weak_order (α : Type u) (lt : α → α → Prop) :
Prop

is_strict_weak_order X lt means that the binary relation lt on X is a strict weak order, that is, is_strict_order X lt and is_incomp_trans X lt.

Instances of this typeclass
source
@[class]
structure is_trichotomous (α : Type u) (lt : α → α → Prop) :
Prop
  • trichotomous : ∀ (a b : α), lt a b ∨ a = b ∨ lt b a

is_trichotomous X lt means that the binary relation lt on X is trichotomous, that is, either lt a b or a = b or lt b a for any a and b.

Instances of this typeclass
source
@[class]
structure is_strict_total_order (α : Type u) (lt : α → α → Prop) :
Prop

is_strict_total_order X lt means that the binary relation lt on X is a strict total order, that is, is_trichotomous X lt and is_strict_order X lt.

Instances of this typeclass
source
@[protected, instance]
def eq_is_equiv (α : Type u) :
is_equiv α eq

Equality is an equivalence relation.

source
theorem irrefl {α : Type u} {r : α → α → Prop} [is_irrefl α r] (a : α) :
¬r a a
source
theorem refl {α : Type u} {r : α → α → Prop} [is_refl α r] (a : α) :
r a a
source
theorem trans {α : Type u} {r : α → α → Prop} [is_trans α r] {a b c : α} :
r a b → r b c → r a c
source
theorem symm {α : 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 → a = b
source
theorem asymm {α : Type u} {r : α → α → Prop} [is_asymm α r] {a b : α} :
r a b → ¬r b a
source
theorem trichotomous {α : Type u} {r : α → α → Prop} [is_trichotomous α r] (a b : α) :
r a b ∨ a = b ∨ r b a
source
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
source
@[protected, instance]
def is_asymm_of_is_trans_of_is_irrefl {α : Type u} {r : α → α → Prop} [is_trans α r] [is_irrefl α r] :
is_asymm α r
source
theorem irrefl_of {α : Type u} (r : α → α → Prop) [is_irrefl α r] (a : α) :
¬r a a
source
theorem refl_of {α : Type u} (r : α → α → Prop) [is_refl α r] (a : α) :
r a a
source
theorem trans_of {α : Type u} (r : α → α → Prop) [is_trans α r] {a b c : α} :
r a b → r b c → r a c
source
theorem symm_of {α : Type u} (r : α → α → Prop) [is_symm α r] {a b : α} :
r a b → r b a
source
theorem asymm_of {α : Type u} (r : α → α → Prop) [is_asymm α r] {a b : α} :
r a b → ¬r b a
source
theorem total_of {α : Type u} (r : α → α → Prop) [is_total α r] (a b : α) :
r a b ∨ r b a
source
theorem trichotomous_of {α : Type u} (r : α → α → Prop) [is_trichotomous α r] (a b : α) :
r a b ∨ a = b ∨ r b a
source
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
source
def strict_weak_order.equiv {α : Type u} {r : α → α → Prop} (a b : α) :
Prop
Equations
Instances for strict_weak_order.equiv
source
theorem strict_weak_order.erefl {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] (a : α) :
strict_weak_order.equiv a a
source
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
source
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
source
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
source
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
source
@[protected, instance]
def strict_weak_order.is_equiv {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r] :
is_equiv α strict_weak_order.equiv
source
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
source
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
source
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
source
theorem eq_of_incomp {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b : α} :
¬lt a b ∧ ¬lt b a → a = b
source
theorem eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b : α} :
strict_weak_order.equiv a b → a = b
source
theorem incomp_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b : α) :
¬lt a b ∧ ¬lt b a ↔ a = b
source
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
source
theorem not_lt_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_order α lt] {a b : α} :
lt a b → ¬lt b a