English
The map finsetClopens X is injective for compact X, i.e., different discrete quotients yield different finite sets of clopen fibers.
Русский
Для компактного X отображение finsetClopens X инъективно: разные дискретные факторизации дают разные конечные множества клабо́пных волокон.
LaTeX
$$$\\text{Injective}(\\mathrm{finsetClopens}(X))$$$
Lean4
/-- A helper lemma to prove that `finsetClopens X` is injective, see `finsetClopens_inj`. -/
theorem comp_finsetClopens [CompactSpace X] :
(Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ Finset.toSet) ∘ finsetClopens X = fun ⟨f, _⟩ ↦ f.classes :=
by
ext d
simp only [Setoid.classes, Set.mem_setOf_eq, Function.comp_apply, finsetClopens, Set.coe_toFinset, Set.mem_image,
Set.mem_range, exists_exists_eq_and]
constructor
· refine fun ⟨y, h⟩ ↦ ⟨Quotient.out (s := d.toSetoid) y, ?_⟩
ext
simpa [← h] using Quotient.mk_eq_iff_out (s := d.toSetoid)
· exact fun ⟨y, h⟩ ↦ ⟨d.proj y, by ext; simp [h, proj]⟩
