English
In a T1 space, a set s is codiscrete within U iff every point z in U has a neighborhood t such that t ∩ (U \ s) is finite.
Русский
В T1-пространстве множество s кодискретно внутри U тогда и только тогда, когда для каждой z в U существует окрестность t такая, что t∩(U\s) конечно.
LaTeX
$$$s \in \text{codiscreteWithin}(U) \iff \forall z \in U, \exists t \in \mathcal{N}(z), \operatorname{Finite}(t \cap (U \setminus s)).$$$
Lean4
/-- In a T1Space, a set `s` is codiscreteWithin `U` iff it has locally finite complement within `U`.
More precisely: `s` is codiscreteWithin `U` iff every point `z ∈ U` has a punctured neighborhood
intersect `U \ s` in only finitely many points. -/
theorem codiscreteWithin_iff_locallyFiniteComplementWithin [T1Space X] {s U : Set X} :
s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ (U \ s)) :=
by
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
constructor
· intro h z h₁z
obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
use insert z t, insert_mem_nhds_iff.mpr h₁t
by_cases hz : z ∈ U \ s
· rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]
simp
· rw [inter_comm, inter_insert_of_notMem hz, inter_comm, h₂t]
simp
· intro h z h₁z
obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
use t \ (t ∩ (U \ s)), nhdsNE_of_nhdsNE_sdiff_finite (mem_nhdsWithin_of_mem_nhds h₁t) h₂t
simp
