Cardinal

📁 Source: Mathlib/Algebra/MvPolynomial/Cardinal.lean

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_eq, cardinalMk_eq_lift, cardinalMk_eq_max, cardinalMk_eq_max_lift, cardinalMk_eq_one, cardinalMk_le_max, cardinalMk_le_max_lift	7
Total	7

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_eq 📖	mathematical	—	MvPolynomial	—	cardinalMk_eq_lift Cardinal.lift_id
cardinalMk_eq_lift 📖	mathematical	—	MvPolynomial Cardinal.lift	—	Equiv.cardinal_eq
cardinalMk_eq_max 📖	mathematical	—	MvPolynomial 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	—	MvPolynomial Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	Cardinal.mk_finsupp_lift_of_infinite Finsupp.infinite_of_right instInfiniteNat Cardinal.mk_finsupp_nat max_assoc Cardinal.lift_max Cardinal.lift_aleph0 max_comm
cardinalMk_eq_one 📖	mathematical	—	MvPolynomial Cardinal Cardinal.instOne	—	Cardinal.mk_eq_one Unique.instSubsingleton
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE MvPolynomial SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	LE.le.trans cardinalMk_le_max_lift Cardinal.lift_id le_refl
cardinalMk_le_max_lift 📖	mathematical	—	Cardinal Cardinal.instLE MvPolynomial SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	subsingleton_or_nontrivial Eq.trans_le Cardinal.mk_eq_one Unique.instSubsingleton 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