Theorems · Definition · general topology
cantorSet
Set ℝ
The Cantor set is the subset of the unit interval obtained as the intersection of all
pre-Cantor sets. This means that the Cantor set is obtained by iteratively removing the
open middle third of each subinterval, starting from the unit interval [0, 1].
- Defined in
- Mathlib.Topology.Instances.CantorSet
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement · cited by 25,697
- Set.iInterproof · cited by 1,084
- preCantorSetproof · cited by 12
Cited by16
Results whose statement or proof uses this declaration.
- cantorSet_subset_unitIntervalstatement · cited by 3
- cantorSequence_mem_cantorSetstatement and proof · cited by 2
- ofDigits_zero_two_sequence_mem_cantorSetstatement · cited by 2
- cantorSet_eq_union_halvesstatement · cited by 1
- cantorStep_mem_cantorSetstatement and proof · cited by 1
- le_ofDigits_cantorToTernary_sumstatement and proof · cited by 1
- isClosed_cantorSetstatement · cited by 1
- ofDigits_cantorToTernarystatement and proof · cited by 1
- ofDigits_cantorToTernary_sum_lestatement and proof · cited by 1
- quarter_mem_cantorSetstatement · cited by 0
- cantorSetEquivNatToBoolstatement and proof · cited by 0
- cantorSetHomeomorphNatToBoolstatement · cited by 0