Theorems · Theorem · logic and foundations
Set.countable_univ
∀ {α : Type u} [Countable α], Set.univ.Countable- Defined in
- Mathlib.Data.Set.Countable
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- Countable
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.
- Set.univstatement and proof · cited by 3,945
- Countablestatement and proof · cited by 633
- Set.Countablestatement · cited by 545
- Set.to_countableproof · cited by 46
Cited by7
Results whose statement or proof uses this declaration.
- MeasureTheory.measurableSet_exists_tendstoproof · cited by 4
- Set.Countable.ofPred_finiteproof · cited by 3
- ZSpan.fundamentalDomain_measurableSetproof · cited by 3
- NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasisproof · cited by 2
- Real.volume_preserving_transvectionStructproof · cited by 1
- MeasureTheory.Measure.pi_pi_auxproof · cited by 1
- MeasureTheory.IsStoppingTime.iInfproof · cited by 0