Cardinality

📁 Source: Mathlib/Algebra/FreeAlgebra/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_adjoin_le, lift_cardinalMk_adjoin_le, cardinalMk_eq, cardinalMk_eq_lift, cardinalMk_eq_max, cardinalMk_eq_max_lift, cardinalMk_eq_one, cardinalMk_le_max, cardinalMk_le_max_lift	9
Total	9

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_adjoin_le 📖	mathematical	—	Cardinal Cardinal.instLE Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Set.Elem Cardinal.aleph0	—	Cardinal.lift_id lift_cardinalMk_adjoin_le
lift_cardinalMk_adjoin_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Set.Elem Cardinal.aleph0	—	Cardinal.mk_range_le_lift adjoin_eq_range_freeAlgebra_lift LE.le.trans Cardinal.lift_id' Cardinal.lift_umax FreeAlgebra.cardinalMk_le_max_lift

FreeAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_eq 📖	mathematical	—	FreeAlgebra	—	cardinalMk_eq_lift Cardinal.lift_id
cardinalMk_eq_lift 📖	mathematical	—	FreeAlgebra Cardinal.lift	—	Cardinal.lift_mk_eq' Equiv.cardinal_eq MonoidAlgebra.eq_1 Cardinal.lift_umax Cardinal.lift_id'
cardinalMk_eq_max 📖	mathematical	—	FreeAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	cardinalMk_eq_max_lift Cardinal.lift_id
cardinalMk_eq_max_lift 📖	mathematical	—	FreeAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	Cardinal.mk_freeMonoid Equiv.cardinal_eq MonoidAlgebra.eq_1 Cardinal.mk_finsupp_lift_of_infinite instInfiniteFreeMonoidOfNonempty Cardinal.lift_max Cardinal.lift_aleph0 sup_comm sup_assoc
cardinalMk_eq_one 📖	mathematical	—	FreeAlgebra Cardinal Cardinal.instOne	—	Equiv.cardinal_eq MonoidAlgebra.eq_1 Cardinal.mk_eq_one Unique.instSubsingleton
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE FreeAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	Cardinal.lift_id cardinalMk_le_max_lift
cardinalMk_le_max_lift 📖	mathematical	—	Cardinal Cardinal.instLE FreeAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	subsingleton_or_nontrivial Eq.trans_le cardinalMk_eq_one le_max_of_le_right Cardinal.one_le_aleph0 isEmpty_or_nonempty cardinalMk_eq_lift le_max_of_le_left le_max_left Eq.le cardinalMk_eq_max_lift

---

← Back to Index