@[class]
- symm_op : ∀ (a b : α), op a b = op b a
@[class]
- comm : ∀ (a b : α), op a b = op b a
@[instance]
def
is_symm_op_of_is_commutative
(α : Type u)
(op : α → α → α)
[is_commutative α op] :
is_symm_op α α op
Equations
- _ = _
@[class]
- assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)
@[class]
- left_id : ∀ (a : α), op o a = a
@[class]
- right_id : ∀ (a : α), op a o = a
@[class]
- left_null : ∀ (a : α), op o a = o
@[class]
- right_null : ∀ (a : α), op a o = o
@[class]
@[class]
@[class]
- idempotent : ∀ (a : α), op a a = a
@[class]
- left_distrib : ∀ (a b c : α), op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c)
@[class]
- right_distrib : ∀ (a b c : α), op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c)
@[class]
- left_inv : ∀ (a : α), op (inv a) a = o
@[class]
- right_inv : ∀ (a : α), op a (inv a) = o
@[class]
- irrefl : ∀ (a : α), ¬r a a
@[class]
- refl : ∀ (a : α), r a a
@[class]
- symm : ∀ (a b : α), r a b → r b a
Instances
@[instance]
Equations
- _ = _
@[class]
- asymm : ∀ (a b : α), r a b → ¬r b a
@[class]
- antisymm : ∀ (a b : α), r a b → r b a → a = b
@[class]
- trans : ∀ (a b c : α), r a b → r b c → r a c
@[class]
- total : ∀ (a b : α), r a b ∨ r b a
@[class]
@[class]
@[instance]
def
is_total_preorder_is_preorder
(α : Type u)
(r : α → α → Prop)
[s : is_total_preorder α r] :
is_preorder α r
Equations
@[class]
- to_is_preorder : is_preorder α r
- to_is_antisymm : is_antisymm α r
@[class]
@[class]
@[class]
- to_is_strict_order : is_strict_order α lt
- to_is_incomp_trans : is_incomp_trans α lt
@[class]
@[class]
- to_is_trichotomous : is_trichotomous α lt
- to_is_strict_weak_order : is_strict_weak_order α lt
theorem
antisymm
{α : Type u}
{r : α → α → Prop}
[is_antisymm α r]
{a b : α} :
r a b → r b a → a = b
@[instance]
def
is_asymm_of_is_trans_of_is_irrefl
{α : Type u}
{r : α → α → Prop}
[is_trans α r]
[is_irrefl α r] :
is_asymm α r
Equations
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 : α) :
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 : α} :
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]
Equations
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 : α} :
theorem
lt_of_incomp_of_lt
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
[decidable_rel lt]
{a b c : α} :
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 : α) :
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