Cardinal

📁 Source: Mathlib/Data/W/Cardinal.lean

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_eq_sum, cardinalMk_eq_sum_lift, cardinalMk_le_max_aleph0_of_finite, cardinalMk_le_max_aleph0_of_finite', cardinalMk_le_of_le, cardinalMk_le_of_le'	6
Total	6

WType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_eq_sum 📖	mathematical	—	WType Cardinal.sum Cardinal Cardinal.instPowCardinal	—	cardinalMk_eq_sum_lift Cardinal.lift_id
cardinalMk_eq_sum_lift 📖	mathematical	—	WType Cardinal.sum Cardinal Cardinal.instPowCardinal Cardinal.lift	—	Cardinal.mk_congr Cardinal.mk_sigma Cardinal.mk_arrow Cardinal.lift_id' Cardinal.lift_umax
cardinalMk_le_max_aleph0_of_finite 📖	mathematical	Finite	Cardinal Cardinal.instLE WType SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	LE.le.trans_eq cardinalMk_le_max_aleph0_of_finite' Cardinal.lift_id
cardinalMk_le_max_aleph0_of_finite' 📖	mathematical	Finite	Cardinal Cardinal.instLE WType SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	isEmpty_or_nonempty Cardinal.mk_eq_zero instIsEmpty zero_le Cardinal.canonicallyOrderedAdd cardinalMk_le_of_le' Cardinal.sum_le_lift_mk_mul_iSup mul_le_mul' CanonicallyOrderedAdd.toMulLeftMono covariant_swap_mul_of_covariant_mul le_max_left le_rfl Cardinal.mul_eq_left le_max_right ciSup_le' Cardinal.pow_le Cardinal.lt_aleph0_of_finite instFiniteULift pos_iff_ne_zero Order.succ_le_iff Cardinal.instNoMaxOrder Cardinal.succ_zero le_trans Cardinal.power_zero Cardinal.power_le_power_left LT.lt.trans_le Cardinal.aleph0_pos le_ciSup Cardinal.bddAbove_range UnivLE.small univLE_of_max UnivLE.self
cardinalMk_le_of_le 📖	mathematical	Cardinal Cardinal.instLE Cardinal.sum Cardinal.instPowCardinal	WType	—	cardinalMk_le_of_le' Cardinal.lift_id
cardinalMk_le_of_le' 📖	mathematical	Cardinal Cardinal.instLE Cardinal.sum Cardinal.instPowCardinal Cardinal.lift	WType	—	Cardinal.inductionOn Cardinal.lift_id' Cardinal.mk_le_of_injective elim_injective Function.Embedding.inj'

---

← Back to Index