English
For a compact space X, for each discrete quotient d on X there is a finite set of clopen subsets of X, obtained by taking the fibers of the quotient projection; this finite family is denoted finsetClopens(d).
Русский
Для компактного пространства X существует конечное семейство растяжимых разложений X на открытые и закрытые множества, задаваемое волокнами проекции тождественных классов дискретного факторизации; обозначается finsetClopens(d).
LaTeX
$$$\\mathrm{finsetClopens}_{X}(d) \\subseteq \\mathrm{Clopens}(X)$ и является конечным множством, равным набору всех волокон проекции $\\mathrm{proj}_d^{-1} (\\{x\\})$ при $x \\in d$.$$
Lean4
/-- If `X` is a compact space, then we associate to any discrete quotient on `X` a finite set of
clopen subsets of `X`, given by the fibers of `proj`.
TODO: prove that these form a partition of `X`
-/
noncomputable def finsetClopens [CompactSpace X] (d : DiscreteQuotient X) : Finset (Clopens X) :=
have : Fintype d := Fintype.ofFinite _
(Set.range (fun (x : d) ↦ ⟨_, d.isClopen_preimage { x }⟩) : Set (Clopens X)).toFinset
