Theorems · Theorem · logic and foundations
Set.countable_singleton
∀ {α : Type u} (a : α), {a}.Countable- Defined in
- Mathlib.Data.Set.Countable
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.Countablestatement · cited by 545
- Set.to_countableproof · cited by 46
Cited by13
Results whose statement or proof uses this declaration.
- IsOpen.isGδproof · cited by 7
- isPathConnected_compl_singleton_of_one_lt_rankproof · cited by 3
- CountableInfClosed.infClosedproof · cited by 3
- MeasureTheory.restrict_compl_singletonproof · cited by 2
- MeasureTheory.Measure.ae_neproof · cited by 2
- MeasureTheory.Measure.ext_of_Ico'proof · cited by 2
- circleIntegral.integral_sub_inv_smul_sub_smulproof · cited by 2
- exists_countable_union_perfect_of_isClosedproof · cited by 1
- Complex.countable_preimage_expproof · cited by 1
- MeasureTheory.Measure.ext_of_Icc'proof · cited by 1
- Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAtproof · cited by 1