English
For finite s, the set π C (· ∈ s) has a finite element type; more precisely, there is a finite type structure on the elements of π C (· ∈ s).
Русский
Для конечного множества s множество π C (⋅ ∈ s) является конечным множеством элементов.
LaTeX
$$$\\text{instFintypeElemForallBoolπMemFinset } : Fintype (π C (\\cdot ∈ s).Elem)$$$
Lean4
/-- The map `Nobeling.ι` is a closed embedding. -/
theorem isClosedEmbedding : IsClosedEmbedding (Nobeling.ι S) :=
by
apply Continuous.isClosedEmbedding
· dsimp +unfoldPartialApp [ι]
refine continuous_pi ?_
intro C
rw [← IsLocallyConstant.iff_continuous]
refine ((IsLocallyConstant.tfae _).out 0 3).mpr ?_
rintro ⟨⟩
· refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)
convert C.2
ext x
simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, decide_eq_false_iff_not, not_not]
· refine IsClopen.isOpen ?_
convert C.2
ext x
simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]
· intro a b h
by_contra hn
obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn
apply hh.2 ∘ of_decide_eq_true
dsimp +unfoldPartialApp [ι] at h
rw [← congr_fun h ⟨C, hC⟩]
exact decide_eq_true hh.1
