Theorems · Theorem · logic and foundations
Set.countable_range
∀ {β : Type v} {ι : Sort x} [Countable ι] (f : ι → β), (Set.range f).Countable- Defined in
- Mathlib.Data.Set.Countable
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses Classical.choice
- Assumes
- Countable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.rangestatement · cited by 4,705
- Countablestatement and proof · cited by 633
- Set.Countablestatement · cited by 545
- Set.rangeFactorization_surjectiveproof · cited by 20
- Function.Surjective.countableproof · cited by 3
- Countable.to_setproof · cited by 3
Cited by31
Results whose statement or proof uses this declaration.
- Set.Countable.imageproof · cited by 47
- Set.countable_iUnionproof · cited by 22
- MeasureTheory.measure_iUnion_null_iffproof · cited by 13
- TopologicalSpace.isOpen_iUnion_countableproof · cited by 9
- IsGδ.iInter_of_isOpenproof · cited by 5
- Set.countable_ofPred_finite_subsetproof · cited by 5
- UniformSpace.subset_countable_closure_of_almost_dense_setproof · cited by 4
- TopologicalSpace.IsSeparable.secondCountableTopologyproof · cited by 4
- CountableSupClosed.iSup_memproof · cited by 3
- countable_iInter_memproof · cited by 3
- CountableInfClosed.iInf_memproof · cited by 3
- Set.countable_iff_exists_subset_rangeproof · cited by 3