mathlib documentation

core.init.algebra.classes

@[class]
structure is_symm_op (α : Type u) (β : out_param (Type v)) :
(α → α → β) → Prop
  • symm_op : ∀ (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_left_id (α : Type u) :
(α → α → α)out_param α → Prop
  • left_id : ∀ (a : α), op o a = a

Instances
@[class]
structure is_right_id (α : Type u) :
(α → α → α)out_param α → Prop
  • right_id : ∀ (a : α), op a o = a

Instances
@[class]
structure is_left_null (α : Type u) :
(α → α → α)out_param α → Prop
  • left_null : ∀ (a : α), op o a = o

@[class]
structure is_right_null (α : Type u) :
(α → α → α)out_param α → Prop
  • right_null : ∀ (a : α), op a o = o

@[class]
structure is_left_cancel (α : Type u) :
(α → α → α) → Prop
  • left_cancel : ∀ (a b c : α), op a b = op a cb = c

Instances
@[class]
structure is_right_cancel (α : Type u) :
(α → α → α) → Prop
  • right_cancel : ∀ (a b c : α), op a b = op c ba = c

Instances
@[class]
structure is_idempotent (α : Type u) :
(α → α → α) → Prop
  • idempotent : ∀ (a : α), op a a = a

Instances
@[class]
structure is_left_distrib (α : Type u) :
(α → α → α)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) :
(α → α → α)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) :
(α → α → α)out_param (α → α)out_param α → Prop
  • left_inv : ∀ (a : α), op (inv a) a = o

@[class]
structure is_right_inv (α : Type u) :
(α → α → α)out_param (α → α)out_param α → Prop
  • right_inv : ∀ (a : α), op a (inv a) = o

@[class]
structure is_cond_left_inv (α : Type u) :
(α → α → α)out_param (α → α)out_param αout_param (α → Prop) → Prop
  • left_inv : ∀ (a : α), p aop (inv a) a = o

@[class]
structure is_cond_right_inv (α : Type u) :
(α → α → α)out_param (α → α)out_param αout_param (α → Prop) → Prop
  • right_inv : ∀ (a : α), p aop a (inv a) = o

@[class]
structure is_distinct (α : Type u) :
α → α → Prop
  • distinct : a b

@[class]
structure is_irrefl (α : Type u) :
(α → α → 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) :
(α → α → 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) :
(α → α → Prop) → Prop
  • symm : ∀ (a b : α), r a br 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) :
(α → α → 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) :
(α → α → Prop) → Prop
  • antisymm : ∀ (a b : α), r a br b aa = b

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

Instances
@[class]
structure is_trans (α : Type u) :
(α → α → Prop) → Prop
  • trans : ∀ (a b c : α), r a br b cr a c

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

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

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) :
(α → α → Prop) → Prop

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

Every total pre-order is a pre-order.

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

Instances
@[class]
structure is_linear_order (α : Type u) :
(α → α → Prop) → Prop

Instances
@[class]
structure is_equiv (α : Type u) :
(α → α → Prop) → Prop

Instances
@[class]
structure is_per (α : Type u) :
(α → α → Prop) → Prop

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

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

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

Instances
@[class]
structure is_strict_total_order (α : Type u) :
(α → α → Prop) → Prop

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 br b cr a c

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

theorem antisymm {α : Type u} {r : α → α → Prop} [is_antisymm α r] {a b : α} :
r a br b aa = 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 br b cr a c

theorem symm_of {α : Type u} (r : α → α → Prop) [is_symm α r] {a b : α} :
r a br 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}, α → α → Prop

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

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

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

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

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

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

theorem is_strict_weak_order_of_is_total_preorder {α : Type u} {le lt : α → α → Prop} [decidable_rel le] [s : is_total_preorder α le] :
(∀ (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 blt 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 alt b clt a c

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

theorem eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {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 : α) :

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