Theorems · Theorem · logic and foundations

Set.Finite.countable

∀ {α : Type u} {s : Set α}, s.Finite → s.Countable

Defined in: Mathlib.Data.Set.Countable
Cited by: 30 results in Mathlib
Foundations: Depth 17 from the axioms · uses Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

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.Elemproof · cited by 7,166
Finiteproof · cited by 3,029
Set.Finitestatement and proof · cited by 1,814
Set.Countablestatement · cited by 545
Set.to_countableproof · cited by 46
Set.Finite.to_subtypeproof · cited by 44

Cited by30

Results whose statement or proof uses this declaration.

Finset.countable_toSetproof · cited by 32
Set.Finite.measure_zeroproof · cited by 9
Set.Finite.isLindelof_biUnionproof · cited by 4
Set.Finite.isSeparableproof · cited by 4
Set.Subsingleton.countableproof · cited by 4
Set.Finite.measurableSet_biUnionproof · cited by 3
FirstOrder.Language.Substructure.FG.cgproof · cited by 3
Set.Finite.isGδ_complproof · cited by 2
Set.Countable.of_subsingletonproof · cited by 2
Set.Finite.measurableSet_biInterproof · cited by 2
Algebraic.cardinalMk_lift_le_mulproof · cited by 2
MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀proof · cited by 2