Continuum

📁 Source: Mathlib/SetTheory/Cardinal/Continuum.lean

Statistics

Metric	Count
Definitions `continuum`, `term𝔠`	2
Theorems `aleph0_add_continuum`, `aleph0_le_continuum`, `aleph0_lt_continuum`, `aleph0_mul_continuum`, `aleph0_power_aleph0`, `aleph_one_le_continuum`, `beth_one`, `continuum_add_aleph0`, `continuum_add_nat`, `continuum_add_ofNat`, `continuum_add_self`, `continuum_le_lift`, `continuum_lt_lift`, `continuum_mul_aleph0`, `continuum_mul_nat`, `continuum_mul_ofNat`, `continuum_mul_self`, `continuum_ne_zero`, `continuum_pos`, `continuum_power_aleph0`, `continuum_toENat`, `continuum_toNat`, `lift_continuum`, `lift_le_continuum`, `lift_lt_continuum`, `mk_set_nat`, `nat_add_continuum`, `nat_lt_continuum`, `nat_mul_continuum`, `nat_power_aleph0`, `ofNat_add_continuum`, `ofNat_mul_continuum`, `power_aleph0_of_le_continuum`, `two_power_aleph0`	34
Total	36

Cardinal

Definitions

Name	Category	Theorems
`continuum` 📖	CompOp	53 math math: `continuum_mul_ofNat`, `mk_Iio_real`, `aleph0_le_continuum`, `nat_add_continuum`, `aleph0_power_aleph0`, `continuum_mul_self`, `aleph_one_le_continuum`, `nat_lt_continuum`, `aleph0_add_continuum`, `continuum_lt_lift`, `nat_mul_continuum`, `continuum_mul_nat`, `ofNat_mul_continuum`, `beth_one`, `mk_real`, `mk_Icc_real`, `continuum_pos`, `continuum_add_self`, `continuum_mul_aleph0`, `ofNat_add_continuum`, `mk_Iic_real`, `aleph0_mul_continuum`, `MeasurableSpace.cardinal_measurableSet_le_continuum`, `IsClosed.two_pow_mk_lt_continuum`, `mk_univ_real`, `MeasurableSpace.cardinal_generateMeasurable_le_continuum`, `continuum_toENat`, `Real.rank_rat_real`, `continuum_le_cardinal_of_nontriviallyNormedField`, `continuum_add_aleph0`, `mk_univ_complex`, `continuum_le_lift`, `mk_set_nat`, `continuum_power_aleph0`, `continuum_add_ofNat`, `continuum_add_nat`, `mk_complex`, `mk_Ioo_real`, `mk_Ici_real`, `IsClosed.mk_lt_continuum`, `Complex.rank_rat_complex`, `two_power_aleph0`, `lift_lt_continuum`, `lift_le_continuum`, `mk_Ico_real`, `continuum_le_cardinal_of_module`, `mk_Ioc_real`, `nat_power_aleph0`, `aleph0_lt_continuum`, `lift_continuum`, `continuum_le_cardinal_of_isOpen`, `mk_Ioi_real`, `continuum_toNat`
`term𝔠` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aleph0_add_continuum` 📖	mathematical	—	`Cardinal` `instAdd` `aleph0` `continuum`	—	`add_eq_right` `aleph0_le_continuum`
`aleph0_le_continuum` 📖	mathematical	—	`Cardinal` `instLE` `aleph0` `continuum`	—	`LT.lt.le` `aleph0_lt_continuum`
`aleph0_lt_continuum` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0` `continuum`	—	`cantor`
`aleph0_mul_continuum` 📖	mathematical	—	`Cardinal` `instMul` `aleph0` `continuum`	—	`mul_comm` `continuum_mul_aleph0`
`aleph0_power_aleph0` 📖	mathematical	—	`Cardinal` `instPowCardinal` `aleph0` `continuum`	—	`power_self_eq` `le_rfl`
`aleph_one_le_continuum` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `continuum`	—	`succ_aleph0` `Order.succ_le_of_lt` `aleph0_lt_continuum`
`beth_one` 📖	mathematical	—	`beth` `Ordinal` `Ordinal.one` `continuum`	—	`Nat.instAtLeastTwoHAddOfNat` `Ordinal.succ_zero` `beth_zero` `beth_succ`
`continuum_add_aleph0` 📖	mathematical	—	`Cardinal` `instAdd` `continuum` `aleph0`	—	`add_comm` `aleph0_add_continuum`
`continuum_add_nat` 📖	mathematical	—	`Cardinal` `instAdd` `continuum` `instNatCast`	—	`add_comm` `nat_add_continuum`
`continuum_add_ofNat` 📖	mathematical	—	`Cardinal` `instAdd` `continuum`	—	`continuum_add_nat`
`continuum_add_self` 📖	mathematical	—	`Cardinal` `instAdd` `continuum`	—	`add_eq_self` `aleph0_le_continuum`
`continuum_le_lift` 📖	mathematical	—	`Cardinal` `instLE` `continuum` `lift`	—	`lift_continuum` `lift_le`
`continuum_lt_lift` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `continuum` `lift`	—	`lift_continuum` `lift_lt`
`continuum_mul_aleph0` 📖	mathematical	—	`Cardinal` `instMul` `continuum` `aleph0`	—	`mul_eq_left` `aleph0_le_continuum` `aleph0_ne_zero`
`continuum_mul_nat` 📖	mathematical	—	`Cardinal` `instMul` `continuum` `instNatCast`	—	`mul_comm` `nat_mul_continuum`
`continuum_mul_ofNat` 📖	mathematical	—	`Cardinal` `instMul` `continuum`	—	`continuum_mul_nat` `OfNat.ofNat_ne_zero` `Nat.instCharZero`
`continuum_mul_self` 📖	mathematical	—	`Cardinal` `instMul` `continuum`	—	`mul_eq_left` `aleph0_le_continuum` `le_rfl` `continuum_ne_zero`
`continuum_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `continuum_pos`
`continuum_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `continuum`	—	`nat_lt_continuum`
`continuum_power_aleph0` 📖	mathematical	—	`Cardinal` `instPowCardinal` `continuum` `aleph0`	—	`Nat.instAtLeastTwoHAddOfNat` `two_power_aleph0` `power_mul` `mul_eq_left` `le_rfl` `aleph0_ne_zero`
`continuum_toENat` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `continuum` `Top.top` `instTopENat`	—	`toENat_eq_top` `aleph0_le_continuum`
`continuum_toNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `continuum`	—	`toNat_apply_of_aleph0_le` `aleph0_le_continuum`
`lift_continuum` 📖	mathematical	—	`lift` `continuum`	—	`Nat.instAtLeastTwoHAddOfNat` `two_power_aleph0` `lift_two_power` `lift_aleph0`
`lift_le_continuum` 📖	mathematical	—	`Cardinal` `instLE` `lift` `continuum`	—	`lift_continuum` `lift_le`
`lift_lt_continuum` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `lift` `continuum`	—	`lift_continuum` `lift_lt`
`mk_set_nat` 📖	mathematical	—	`Set` `continuum`	—	`Nat.instAtLeastTwoHAddOfNat` `mk_set` `mk_eq_aleph0` `instCountableNat` `instInfiniteNat`
`nat_add_continuum` 📖	mathematical	—	`Cardinal` `instAdd` `instNatCast` `continuum`	—	`nat_add_eq` `aleph0_le_continuum`
`nat_lt_continuum` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instNatCast` `continuum`	—	`LT.lt.trans` `natCast_lt_aleph0` `aleph0_lt_continuum`
`nat_mul_continuum` 📖	mathematical	—	`Cardinal` `instMul` `instNatCast` `continuum`	—	`mul_eq_right` `aleph0_le_continuum` `LT.lt.le` `nat_lt_continuum` `Nat.cast_ne_zero` `instCharZero`
`nat_power_aleph0` 📖	mathematical	—	`Cardinal` `instPowCardinal` `instNatCast` `aleph0` `continuum`	—	`nat_power_eq` `le_rfl`
`ofNat_add_continuum` 📖	mathematical	—	`Cardinal` `instAdd` `continuum`	—	`nat_add_continuum`
`ofNat_mul_continuum` 📖	mathematical	—	`Cardinal` `instMul` `continuum`	—	`nat_mul_continuum` `OfNat.ofNat_ne_zero` `Nat.instCharZero`
`power_aleph0_of_le_continuum` 📖	mathematical	`Cardinal` `instLE` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `continuum`	`instPowCardinal` `aleph0`	—	`Nat.instAtLeastTwoHAddOfNat` `le_antisymm` `continuum_power_aleph0` `power_le_power_right` `two_power_aleph0`
`two_power_aleph0` 📖	mathematical	—	`Cardinal` `instPowCardinal` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `aleph0` `continuum`	—	`Nat.instAtLeastTwoHAddOfNat`

---

← Back to Index