English
Discrete quotients of a compact space X are in bijection with a subset of Finset(Clopens X); there is an explicit equivalence between DiscreteQuotient X and the image of finsetClopens X.
Русский
Дискретные факторизации компактного пространства X образуют биекцию с подмножеством Finset(Clopens X); существует явное эквивалентность между DiscreteQuotient X и образом finsetClopens X.
LaTeX
$$Equiv(DiscreteQuotient X) (Set.range (DiscreteQuotient.finsetClopens X)).Elem$$
Lean4
/-- `finsetClopens X` is injective. -/
theorem finsetClopens_inj [CompactSpace X] : (finsetClopens X).Injective :=
by
apply Function.Injective.of_comp (f := Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ Finset.toSet)
rw [comp_finsetClopens]
intro ⟨_, _⟩ ⟨_, _⟩ h
congr
rw [Setoid.classes_inj]
exact h
