Cardinal

Statistics

Metric	Count
Definitions	0
Theorems `cardinalMk_eq_max`, `cardinalMk_le_max`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinalMk_eq_max` 📖	mathematical	—	`Polynomial` `Cardinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0`	—	`Equiv.cardinal_eq` `AddMonoidAlgebra.eq_1` `Cardinal.mk_finsupp_lift_of_infinite` `instInfiniteNat` `Cardinal.lift_uzero` `max_comm`
`cardinalMk_le_max` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Polynomial` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0`	—	`subsingleton_or_nontrivial` `Eq.trans_le` `Cardinal.mk_eq_one` `Unique.instSubsingleton` `le_max_of_le_right` `Cardinal.one_le_aleph0` `Eq.le` `cardinalMk_eq_max`

---