English
If s is codiscrete within U and U is closed, then U \ s is closed.
Русский
Если s кодискретно внутри U и U замкнуто, тогда U \ s замкнуто.
LaTeX
$$$ s \in \text{codiscreteWithin}(U) \quad \&\quad \text{IsClosed}(U) \Rightarrow \text{IsClosed}(U \setminus s). $$$
Lean4
/-- If `U` is closed and `s` is codiscrete within `U`, then `U \ s` is closed. -/
theorem isClosed_sdiff_of_codiscreteWithin {s U : Set X} (hs : s ∈ codiscreteWithin U) (hU : IsClosed U) :
IsClosed (U \ s) := by
rw [← isOpen_compl_iff, isOpen_iff_eventually]
intro x hx
by_cases h₁x : x ∈ U
· rw [mem_codiscreteWithin] at hs
filter_upwards [eventually_nhdsWithin_iff.1 (disjoint_principal_right.1 (hs x h₁x))]
intro a ha
by_cases h₂a : a = x
· tauto_set
· specialize ha h₂a
tauto_set
· rw [eventually_iff_exists_mem]
use Uᶜ, hU.compl_mem_nhds h₁x
intro y hy
tauto_set
