English
If s is codiscrete within U, then the intersection of the complement of s with U, namely s^c ∩ U, carries the discrete topology as a subspace of X.
Русский
Если множество s кодискретно внутри U, то пересечение комплемента s с U, то есть s^c ∩ U, имеет дискретную топологию как подпространство X.
LaTeX
$$$ s \in \text{codiscreteWithin}(U) \;\Rightarrow\; \text{DiscreteTopology}((s^{c} \cap U) : \text{Set} X). $$$
Lean4
/-- If `s` is codiscrete within `U`, then `sᶜ ∩ U` has discrete topology. -/
theorem discreteTopology_of_codiscreteWithin {U s : Set X} (h : s ∈ Filter.codiscreteWithin U) :
DiscreteTopology ((sᶜ ∩ U) : Set X) :=
by
rw [(by simp : ((sᶜ ∩ U) : Set X) = ((s ∪ Uᶜ)ᶜ : Set X)), discreteTopology_subtype_iff]
simp_rw [mem_codiscreteWithin, Filter.disjoint_principal_right] at h
intro x hx
rw [← Filter.mem_iff_inf_principal_compl, ← Set.compl_diff]
simp_all only [h x, Set.compl_union, compl_compl, Set.mem_inter_iff, Set.mem_compl_iff]
