CantorSet

📁 Source: Mathlib/Topology/Instances/CantorSet.lean

Statistics

Metric	Count
Definitions `cantorSequence`, `cantorSet`, `cantorSetEquivNatToBool`, `cantorSetHomeomorphNatToBool`, `cantorSpaceHomeomorphNatToCantorSpace`, `cantorStep`, `cantorToBinary`, `cantorToTernary`, `preCantorSet`	9
Theorems `cantorSequence_eq_self_sub_sum_cantorToTernary`, `cantorSequence_get_succ`, `cantorSequence_mem_cantorSet`, `cantorSet_eq_union_halves`, `cantorSet_eq_zero_two_ofDigits`, `cantorSet_subset_unitInterval`, `cantorStep_mem_cantorSet`, `cantorToTernary_ne_one`, `isClosed_cantorSet`, `isClosed_preCantorSet`, `isCompact_cantorSet`, `le_ofDigits_cantorToTernary_sum`, `ofDigits_bool_to_fin_three_mem_cantorSet`, `ofDigits_cantorToTernary`, `ofDigits_cantorToTernary_sum_le`, `ofDigits_zero_two_sequence_mem_cantorSet`, `ofDigits_zero_two_sequence_unique`, `preCantorSet_antitone`, `preCantorSet_subset_unitInterval`, `preCantorSet_succ`, `preCantorSet_zero`, `quarter_mem_cantorSet`, `quarter_mem_preCantorSet`, `quarters_mem_preCantorSet`, `zero_mem_cantorSet`, `zero_mem_preCantorSet`	26
Total	35

(root)

Definitions

Name	Category	Theorems
`cantorSequence` 📖	CompOp	3 math math: `cantorSequence_mem_cantorSet`, `cantorSequence_eq_self_sub_sum_cantorToTernary`, `cantorSequence_get_succ`
`cantorSet` 📖	CompOp	11 math math: `ofDigits_zero_two_sequence_mem_cantorSet`, `cantorStep_mem_cantorSet`, `zero_mem_cantorSet`, `ofDigits_bool_to_fin_three_mem_cantorSet`, `cantorSet_eq_zero_two_ofDigits`, `cantorSequence_mem_cantorSet`, `isClosed_cantorSet`, `cantorSet_subset_unitInterval`, `isCompact_cantorSet`, `cantorSet_eq_union_halves`, `quarter_mem_cantorSet`
`cantorSetEquivNatToBool` 📖	CompOp	—
`cantorSetHomeomorphNatToBool` 📖	CompOp	—
`cantorSpaceHomeomorphNatToCantorSpace` 📖	CompOp	—
`cantorStep` 📖	CompOp	1 math math: `cantorStep_mem_cantorSet`
`cantorToBinary` 📖	CompOp	—
`cantorToTernary` 📖	CompOp	5 math math: `ofDigits_cantorToTernary`, `le_ofDigits_cantorToTernary_sum`, `ofDigits_cantorToTernary_sum_le`, `cantorSequence_eq_self_sub_sum_cantorToTernary`, `cantorSequence_get_succ`
`preCantorSet` 📖	CompOp	8 math math: `quarters_mem_preCantorSet`, `isClosed_preCantorSet`, `preCantorSet_subset_unitInterval`, `preCantorSet_antitone`, `zero_mem_preCantorSet`, `preCantorSet_succ`, `quarter_mem_preCantorSet`, `preCantorSet_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cantorSequence_eq_self_sub_sum_cantorToTernary` 📖	mathematical	—	`Stream'.get` `Real` `cantorSequence` `Real.instMul` `Real.instSub` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.ofDigitsTerm` `cantorToTernary` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_zero` `pow_zero` `mul_one` `cantorSequence_get_succ` `Finset.sum_range_succ` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast`
`cantorSequence_get_succ` 📖	mathematical	—	`Stream'.get` `Real` `cantorSequence` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instSub` `Monoid.toPow` `Real.instMonoid` `Real.ofDigitsTerm` `cantorToTernary`	—	`Nat.instAtLeastTwoHAddOfNat` `CharP.cast_eq_zero` `CharP.ofCharZero` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `sub_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`
`cantorSequence_mem_cantorSet` 📖	mathematical	`Real` `Set` `Set.instMembership` `cantorSet`	`Real` `Set` `Set.instMembership` `cantorSet` `Stream'.get` `cantorSequence`	—	`cantorStep_mem_cantorSet`
`cantorSet_eq_union_halves` 📖	mathematical	—	`cantorSet` `Set` `Real` `Set.instUnion` `Set.image` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.image_iInter` `mulRight_bijective₀` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Function.Bijective.comp` `AddGroup.addLeft_bijective` `Set.iInter_union_of_antitone` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Monotone.comp_antitone` `Set.monotone_image` `preCantorSet_antitone` `Antitone.iInter_nat_add`
`cantorSet_eq_zero_two_ofDigits` 📖	mathematical	—	`cantorSet` `setOf` `Real` `Real.ofDigits`	—	`Set.ext` `cantorToTernary_ne_one` `ofDigits_cantorToTernary` `ofDigits_zero_two_sequence_mem_cantorSet`
`cantorSet_subset_unitInterval` 📖	mathematical	—	`Set` `Real` `Set.instHasSubset` `cantorSet` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne`	—	`Set.iInter_subset`
`cantorStep_mem_cantorSet` 📖	mathematical	`Real` `Set` `Set.instMembership` `cantorSet`	`Real` `Set` `Set.instMembership` `cantorSet` `cantorStep`	—	`Nat.instAtLeastTwoHAddOfNat` `cantorSet_eq_union_halves`
`cantorToTernary_ne_one` 📖	—	—	—	—	—
`isClosed_cantorSet` 📖	mathematical	—	`IsClosed` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cantorSet`	—	`isClosed_iInter` `isClosed_preCantorSet`
`isClosed_preCantorSet` 📖	mathematical	—	`IsClosed` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `preCantorSet`	—	`IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Nat.instAtLeastTwoHAddOfNat` `one_div` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `isClosed_Icc` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsClosed.union` `Set.image_congr` `div_eq_inv_mul` `mul_one` `Homeomorph.mulLeft₀.congr_simp` `Topology.IsClosedEmbedding.isClosed_iff_image_isClosed` `Homeomorph.isClosedEmbedding`
`isCompact_cantorSet` 📖	mathematical	—	`IsCompact` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cantorSet`	—	`IsCompact.of_isClosed_subset` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `isClosed_cantorSet` `cantorSet_subset_unitInterval`
`le_ofDigits_cantorToTernary_sum` 📖	mathematical	`Real` `Set` `Set.instMembership` `cantorSet`	`Real` `Real.instLE` `Real.instSub` `Monoid.toPow` `Real.instMonoid` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.ofDigitsTerm` `cantorToTernary`	—	`cantorSequence_mem_cantorSet` `Nat.instAtLeastTwoHAddOfNat` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `sub_mul` `inv_pow` `inv_mul_cancel₀` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsStrictOrderedRing.toCharZero` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `cantorSet_subset_unitInterval` `cantorSequence_eq_self_sub_sum_cantorToTernary` `Mathlib.Tactic.Linarith.sub_neg_of_lt`
`ofDigits_bool_to_fin_three_mem_cantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `cantorSet` `Real.ofDigits`	—	`ofDigits_zero_two_sequence_mem_cantorSet`
`ofDigits_cantorToTernary` 📖	mathematical	`Real` `Set` `Set.instMembership` `cantorSet`	`Real.ofDigits` `Stream'.get` `cantorToTernary`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_iff_tendsto_nat_of_summable_norm` `Real.norm_of_nonneg` `Real.ofDigitsTerm_nonneg` `Real.summable_ofDigitsTerm` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `instOrderTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `tendsto_sub_nhds_zero_iff` `instIsTopologicalAddGroupReal` `sub_sub_cancel_left` `neg_zero` `Filter.Tendsto.neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `tendsto_pow_atTop_nhds_zero_of_abs_lt_one` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_abs_nonneg` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `tendsto_const_nhds` `le_ofDigits_cantorToTernary_sum` `ofDigits_cantorToTernary_sum_le`
`ofDigits_cantorToTernary_sum_le` 📖	mathematical	`Real` `Set` `Set.instMembership` `cantorSet`	`Real` `Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.ofDigitsTerm` `cantorToTernary`	—	`cantorSequence_mem_cantorSet` `Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `Real.instIsOrderedRing` `Real.instNontrivial` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `cantorSet_subset_unitInterval` `cantorSequence_eq_self_sub_sum_cantorToTernary`
`ofDigits_zero_two_sequence_mem_cantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `cantorSet` `Real.ofDigits`	—	`Real.ofDigits_nonneg` `Real.ofDigits_le_one` `Nat.instAtLeastTwoHAddOfNat` `Real.ofDigits_eq_sum_add_ofDigits` `Finset.sum_congr` `Finset.sum_singleton` `zero_add` `pow_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Fintype.complete` `CharP.cast_eq_zero` `CharP.ofCharZero` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`ofDigits_zero_two_sequence_unique` 📖	—	`Real.ofDigits`	—	—	`Function.ne_iff` `Nat.find_min` `Nat.find_spec` `Finset.sum_congr` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Nat.cast_one` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `neg_eq_zero` `Mathlib.Tactic.CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.add_subst` `Mathlib.Tactic.CancelDenoms.mul_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.CancelDenoms.div_subst` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Linarith.mul_eq` `Real.instIsOrderedRing` `sub_eq_zero_of_eq` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.nnrat_rawCast` `Finset.sum_range_succ` `Real.ofDigits_eq_sum_add_ofDigits` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `ne_of_gt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `CharP.cast_eq_zero` `CharP.ofCharZero` `pow_succ` `mul_inv_rev` `MulZeroClass.zero_mul` `inv_pow` `one_div` `zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.ofDigits_nonneg` `Real.ofDigits_le_one`
`preCantorSet_antitone` 📖	mathematical	—	`Antitone` `Set` `Real` `Nat.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `preCantorSet`	—	`antitone_nat_of_succ_le`
`preCantorSet_subset_unitInterval` 📖	mathematical	—	`Set` `Real` `Set.instHasSubset` `preCantorSet` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne`	—	`preCantorSet_zero` `preCantorSet_antitone` `Nat.instCanonicallyOrderedAdd`
`preCantorSet_succ` 📖	mathematical	—	`preCantorSet` `Set` `Real` `Set.instUnion` `Set.image` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instAdd`	—	—
`preCantorSet_zero` 📖	mathematical	—	`preCantorSet` `Set.Icc` `Real` `Real.instPreorder` `Real.instZero` `Real.instOne`	—	—
`quarter_mem_cantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `cantorSet` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.mem_iInter` `quarter_mem_preCantorSet`
`quarter_mem_preCantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `preCantorSet` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `quarters_mem_preCantorSet`
`quarters_mem_preCantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `preCantorSet` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isRat_le_true` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_eq_true` `Mathlib.Meta.NormNum.isNNRat_add`
`zero_mem_cantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `cantorSet` `Real.instZero`	—	—
`zero_mem_preCantorSet` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `preCantorSet` `Real.instZero`	—	`instReflLe` `Real.instZeroLEOneClass` `zero_div`

---

← Back to Index