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.
- comm : ∀ (a b : α), op a b = op b a
Instances of this typeclass
- option.lift_or_get_comm
- xor.is_commutative
- comm_semigroup.to_is_commutative
- add_comm_semigroup.to_is_commutative
- sup_is_commutative
- inf_is_commutative
- set.union_is_comm
- set.inter_is_comm
- finset.has_union.union.is_commutative
- gcd_monoid.gcd.is_commutative
- gcd_monoid.lcm.is_commutative
- symm_diff_is_comm
- assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)
Instances of this typeclass
- option.lift_or_get_assoc
- semigroup.to_is_associative
- add_semigroup.to_is_associative
- equiv.arrow_congr.is_associative
- sup_is_associative
- inf_is_associative
- set.union_is_assoc
- set.inter_is_assoc
- list.has_append.append.is_associative
- finset.has_union.union.is_associative
- gcd_monoid.gcd.is_associative
- gcd_monoid.lcm.is_associative
- symm_diff_is_assoc
- left_null : ∀ (a : α), op o a = o
- right_null : ∀ (a : α), op a o = o
Instances of this typeclass
Instances of this typeclass
- idempotent : ∀ (a : α), op a a = a
- left_distrib : ∀ (a b c : α), op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c)
- right_distrib : ∀ (a b c : α), op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c)
- left_inv : ∀ (a : α), op (inv a) a = o
- right_inv : ∀ (a : α), op a (inv a) = o
- 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
- is_strict_order.to_is_irrefl
- is_well_order.is_irrefl
- is_nonstrict_strict_order.to_is_irrefl
- has_lt.lt.is_irrefl
- gt.is_irrefl
- set.has_ssubset.ssubset.is_irrefl
- subrel.is_irrefl
- finset.has_ssubset.ssubset.is_irrefl
- well_founded.has_well_founded.r.is_irrefl
- covby.is_irrefl
- sum.lift_rel.is_irrefl
- sum.lex.is_irrefl
- colex.has_lt.lt.is_irrefl
- sigma.lex.is_irrefl
- pgame.lf.is_irrefl
- pgame.fuzzy.is_irrefl
- refl : ∀ (a : α), r a a
is_refl X r
means the binary relation r
on X
is reflexive.
Instances of this typeclass
- is_preorder.to_is_refl
- is_total.to_is_refl
- iff.is_refl
- prod.is_refl_left
- prod.is_refl_right
- prod.is_refl_preimage_fst
- prod.is_refl_preimage_snd
- has_le.le.is_refl
- ge.is_refl
- set.has_subset.subset.is_refl
- subrel.is_refl
- relation.refl_gen.is_refl
- relation.refl_trans_gen.is_refl
- list.sublist_forall₂.is_refl
- finset.has_subset.subset.is_refl
- wcovby.is_refl
- sum.lift_rel.is_refl
- sum.lex.is_refl
- measure_theory.measure.absolutely_continuous.is_refl
- sigma.lex.is_refl
- first_order.language.Theory.semantically_equivalent.is_refl
- 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
The opposite of a symmetric relation is symmetric.
- 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
- is_partial_order.to_is_antisymm
- prod.lex.is_antisymm
- has_lt.lt.is_antisymm
- gt.is_antisymm
- has_le.le.is_antisymm
- ge.is_antisymm
- set.has_subset.subset.is_antisymm
- finset.has_subset.subset.is_antisymm
- encodable.order.preimage.is_antisymm
- sum.lift_rel.is_antisymm
- sum.lex.is_antisymm
- sigma.lex.is_antisymm
- 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
- is_preorder.to_is_trans
- is_total_preorder.to_is_trans
- is_per.to_is_trans
- is_strict_order.to_is_trans
- is_well_order.is_trans
- iff.is_trans
- prod.lex.is_trans
- prod.is_trans_preimage_fst
- prod.is_trans_preimage_snd
- has_le.le.is_trans
- ge.is_trans
- has_lt.lt.is_trans
- gt.is_trans
- set.has_subset.subset.is_trans
- set.has_ssubset.ssubset.is_trans
- subrel.is_trans
- relation.trans_gen.is_trans
- relation.refl_trans_gen.is_trans
- list.sublist_forall₂.is_trans
- finset.has_subset.subset.is_trans
- finset.has_ssubset.ssubset.is_trans
- encodable.order.preimage.is_trans
- sum.lift_rel.is_trans
- sum.lex.is_trans
- colex.has_lt.lt.is_trans
- sigma.lex.is_trans
- pgame.subsequent.is_trans
- 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
- is_total_preorder.to_is_total
- is_linear_order.to_is_total
- prod.is_total_left
- prod.is_total_right
- has_le.le.is_total
- ge.is_total
- order_dual.is_total_le
- Prop.le_is_total
- with_bot.is_total_le
- with_top.is_total_le
- encodable.order.preimage.is_total
- enat.has_le.le.is_total
- sum.lex.is_total
- sigma.lex.is_total
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
is_total_preorder X r
means that the binary relation r
on X
is total and a preorder.
Instances of this typeclass
Every total pre-order is a pre-order.
- to_is_preorder : is_preorder α r
- to_is_antisymm : is_antisymm α r
- to_is_partial_order : is_partial_order α r
- to_is_total : is_total α r
Instances of this typeclass
Instances of this typeclass
- to_is_strict_order : is_strict_order α lt
- to_is_incomp_trans : is_incomp_trans α lt
Instances of this typeclass
Instances of this typeclass
- is_strict_total_order.to_is_trichotomous
- is_strict_total_order'.to_is_trichotomous
- is_well_order.is_trichotomous
- has_lt.lt.is_trichotomous
- gt.is_trichotomous
- has_le.le.is_trichotomous
- ge.is_trichotomous
- list.lex.is_trichotomous
- sum.lex.is_trichotomous
- colex.has_lt.lt.is_trichotomous
- sigma.lex.is_trichotomous
- game.lf.is_trichotomous
- to_is_trichotomous : is_trichotomous α lt
- to_is_strict_weak_order : is_strict_weak_order α lt
Equations
- strict_weak_order.equiv a b = (¬r a b ∧ ¬r b a)