Theorems · Definition · logic and foundations
Set.Countable.toEncodable
{α : Type u} → {s : Set α} → s.Countable → Encodable ↑sConvert Set.Countable s to Encodable s (noncomputable).
- Defined in
- Mathlib.Data.Set.Countable
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemstatement · cited by 7,166
- Set.Countablestatement and proof · cited by 545
- Encodablestatement · cited by 140
- Set.Countable.nonempty_encodableproof · cited by 0
Cited by22
Results whose statement or proof uses this declaration.
- VitaliFamily.measure_le_of_frequently_leproof · cited by 5
- MeasureTheory.addHaar_image_le_mul_of_det_ltproof · cited by 4
- dimH_bUnionproof · cited by 4
- countable_bInter_memproof · cited by 4
- Measurable.biSupproof · cited by 3
- MeasureTheory.measure_biUnion₀proof · cited by 3
- MeasureTheory.lintegral_biUnion₀proof · cited by 2
- Filter.EventuallyLE.countable_bInterproof · cited by 2
- Filter.EventuallyLE.countable_bUnionproof · cited by 2
- MeasureTheory.Measure.restrict_biUnion_congrproof · cited by 2
- MeasureTheory.ae_eq_zero_of_forall_dual_of_isSeparableproof · cited by 2
- vadd_singleton_mem_nhds_of_sigmaCompactproof · cited by 1