Cardinality

📁 Source: Mathlib/Analysis/Real/Cardinality.lean

Statistics

Metric	Count
Definitions `cantorFunction`, `cantorFunctionAux`	2
Theorems `Icc_countable_iff`, `Ico_countable_iff`, `Ioc_countable_iff`, `Ioo_countable_iff`, `cantorFunctionAux_eq`, `cantorFunctionAux_false`, `cantorFunctionAux_nonneg`, `cantorFunctionAux_succ`, `cantorFunctionAux_true`, `cantorFunctionAux_zero`, `cantorFunction_injective`, `cantorFunction_le`, `cantorFunction_succ`, `increasing_cantorFunction`, `instUncountableReal`, `mk_Icc_real`, `mk_Ici_real`, `mk_Ico_real`, `mk_Iic_real`, `mk_Iio_real`, `mk_Ioc_real`, `mk_Ioi_real`, `mk_Ioo_real`, `mk_real`, `mk_univ_real`, `not_countable_real`, `summable_cantor_function`	27
Total	29

Cardinal

Definitions

Name	Category	Theorems
`cantorFunction` 📖	CompOp	4 math math: `increasing_cantorFunction`, `cantorFunction_succ`, `cantorFunction_injective`, `cantorFunction_le`
`cantorFunctionAux` 📖	CompOp	7 math math: `cantorFunctionAux_eq`, `cantorFunctionAux_false`, `cantorFunctionAux_nonneg`, `cantorFunctionAux_succ`, `cantorFunctionAux_true`, `cantorFunctionAux_zero`, `summable_cantor_function`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cantorFunctionAux_eq` 📖	mathematical	—	`cantorFunctionAux`	—	—
`cantorFunctionAux_false` 📖	mathematical	—	`cantorFunctionAux` `Real` `Real.instZero`	—	—
`cantorFunctionAux_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`cantorFunctionAux`	—	`cantorFunctionAux_false` `cantorFunctionAux_true` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`cantorFunctionAux_succ` 📖	mathematical	—	`cantorFunctionAux` `Real` `Real.instMul`	—	`cantorFunctionAux_false` `MulZeroClass.mul_zero` `cantorFunctionAux_true` `pow_succ'`
`cantorFunctionAux_true` 📖	mathematical	—	`cantorFunctionAux` `Real` `Monoid.toNatPow` `Real.instMonoid`	—	—
`cantorFunctionAux_zero` 📖	mathematical	—	`cantorFunctionAux` `Real` `Real.instOne` `Real.instZero`	—	`cantorFunctionAux_false` `cantorFunctionAux_true` `pow_zero`
`cantorFunction_injective` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`cantorFunction`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Contrapose.contrapose₁` `Function.ne_iff` `of_not_not` `Nat.find_min` `ne_of_lt` `increasing_cantorFunction` `Bool.eq_true_of_not_eq_false` `Nat.find_spec` `ne_of_gt` `Bool.eq_false_of_not_eq_true`
`cantorFunction_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`cantorFunction`	—	`Summable.tsum_le_tsum` `Real.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `SummationFilter.instNeBotUnconditional` `cantorFunctionAux_false` `cantorFunctionAux_nonneg` `cantorFunctionAux_true` `summable_cantor_function`
`cantorFunction_succ` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`cantorFunction` `Real.instAdd` `Real.instMul`	—	`cantorFunction.eq_1` `Summable.tsum_eq_zero_add` `instIsTopologicalAddGroupReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable_cantor_function` `cantorFunctionAux_succ` `tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `cantorFunctionAux.eq_1` `pow_zero`
`increasing_cantorFunction` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`cantorFunction`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.trans` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.instAtLeastTwo` `LE.le.trans_lt` `cantorFunction_le` `le_of_lt` `lt_of_lt_of_le` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `lt_sub_iff_add_lt` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `cantorFunction_succ` `div_eq_mul_inv` `tsum_geometric_of_lt_one` `zero_add` `tsum_eq_single` `SummationFilter.instLeAtTopUnconditional` `cantorFunctionAux_false` `cantorFunctionAux_zero` `LT.lt.le` `add_lt_add_right` `mul_lt_mul_of_pos_left`
`instUncountableReal` 📖	mathematical	—	`Uncountable` `Real`	—	`aleph0_lt_mk_iff` `mk_real` `aleph0_lt_continuum`
`mk_Icc_real` 📖	mathematical	`Real` `Real.instLT`	`Set.Elem` `Set.Icc` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `mk_le_mk_of_subset` `Set.Ioo_subset_Icc_self` `mk_Ioo_real`
`mk_Ici_real` 📖	mathematical	—	`Set.Elem` `Real` `Set.Ici` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `mk_le_mk_of_subset` `Set.Ioi_subset_Ici_self` `mk_Ioi_real`
`mk_Ico_real` 📖	mathematical	`Real` `Real.instLT`	`Set.Elem` `Set.Ico` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `mk_le_mk_of_subset` `Set.Ioo_subset_Ico_self` `mk_Ioo_real`
`mk_Iic_real` 📖	mathematical	—	`Set.Elem` `Real` `Set.Iic` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `mk_le_mk_of_subset` `Set.Iio_subset_Iic_self` `mk_Iio_real`
`mk_Iio_real` 📖	mathematical	—	`Set.Elem` `Real` `Set.Iio` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `Set.image_const_sub_Iio` `Real.instIsOrderedAddMonoid` `add_sub_cancel_right` `mk_image_le` `mk_Ioi_real`
`mk_Ioc_real` 📖	mathematical	`Real` `Real.instLT`	`Set.Elem` `Set.Ioc` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `mk_le_mk_of_subset` `Set.Ioo_subset_Ioc_self` `mk_Ioo_real`
`mk_Ioi_real` 📖	mathematical	—	`Set.Elem` `Real` `Set.Ioi` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `not_lt` `ne_of_lt` `Set.Iio_union_right` `Set.Iic_union_Ioi` `lt_imp_lt_of_le_of_le` `mk_union_le` `le_refl` `add_le_add_left` `addRightMono` `Set.image_const_sub_Ioi` `Real.instIsOrderedAddMonoid` `add_sub_cancel_right` `add_lt_of_lt` `LT.lt.le` `Nat.instAtLeastTwoHAddOfNat` `cantor` `LE.le.trans_lt` `mk_image_le` `mk_singleton` `LT.lt.trans` `one_lt_aleph0` `mk_univ_real`
`mk_Ioo_real` 📖	mathematical	`Real` `Real.instLT`	`Set.Elem` `Set.Ioo` `Real.instPreorder` `continuum`	—	`le_antisymm` `mk_set_le` `mk_real` `mk_image_le` `le_trans` `Set.image_sub_const_Ioo` `Real.instIsOrderedAddMonoid` `sub_self` `sub_pos_of_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Set.image_inv_eq_inv` `Set.inv_Ioo_0_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mk_Ioi_real` `le_refl`
`mk_real` 📖	mathematical	—	`Real` `continuum`	—	`le_antisymm` `Rat.instIsStrictOrderedRing` `IsAbsoluteValue.abs_isAbsoluteValue` `Equiv.cardinal_eq` `LE.le.trans` `mk_quotient_le` `LE.le.trans_eq` `mk_subtype_le` `power_def` `mk_nat` `mkRat` `aleph0_power_aleph0` `Nat.instAtLeastTwoHAddOfNat` `mk_bool` `two_power_aleph0` `mk_le_of_injective` `cantorFunction_injective` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.instAtLeastTwo`
`mk_univ_real` 📖	mathematical	—	`Set.Elem` `Real` `Set.univ` `continuum`	—	`mk_univ` `mk_real`
`not_countable_real` 📖	mathematical	—	`Set.Countable` `Real` `Set.univ`	—	`Set.not_countable_univ` `instUncountableReal`
`summable_cantor_function` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cantorFunctionAux` `SummationFilter.unconditional`	—	`Summable.summable_of_eq_zero_or_self` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `summable_geometric_of_lt_one` `cantorFunctionAux_false` `cantorFunctionAux_true` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instNontrivial`

Cardinal.Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_countable_iff` 📖	mathematical	—	`Set.Countable` `Real` `Set.Icc` `Real.instPreorder` `Real.instLE`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Cardinal.le_aleph0_iff_set_countable` `Cardinal.mk_Icc_real` `not_le` `Cardinal.aleph0_lt_continuum` `le_iff_eq_or_lt` `Set.Icc_self` `Set.Icc_eq_empty`
`Ico_countable_iff` 📖	mathematical	—	`Set.Countable` `Real` `Set.Ico` `Real.instPreorder` `Real.instLE`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Cardinal.le_aleph0_iff_set_countable` `Cardinal.mk_Ico_real` `not_le` `Cardinal.aleph0_lt_continuum` `Set.Ico_eq_empty`
`Ioc_countable_iff` 📖	mathematical	—	`Set.Countable` `Real` `Set.Ioc` `Real.instPreorder` `Real.instLE`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Cardinal.le_aleph0_iff_set_countable` `Cardinal.mk_Ioc_real` `not_le` `Cardinal.aleph0_lt_continuum` `Set.Ioc_eq_empty`
`Ioo_countable_iff` 📖	mathematical	—	`Set.Countable` `Real` `Set.Ioo` `Real.instPreorder` `Real.instLE`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Cardinal.le_aleph0_iff_set_countable` `Cardinal.mk_Ioo_real` `not_le` `Cardinal.aleph0_lt_continuum` `Set.Ioo_eq_empty`

---

← Back to Index