English
A set s is codiscrete within U if and only if, for every z in U, there exists a punctured neighborhood t of z such that t does not meet U \ s.
Русский
Множество s кодискретно внутри U тогда и только тогда, если для каждого z из U существует дырявая окрестность t(z), такая что t(z) не пересекает U \ s.
LaTeX
$$$ s \in \text{codiscreteWithin}(U) \iff \forall z \in U, \exists t \in \mathcal{N}^{\neq}_z,\ t \cap (U \setminus s) = \emptyset. $$$
Lean4
/-- Helper lemma for `codiscreteWithin_iff_locallyFiniteComplementWithin`: A set `s` is
`codiscreteWithin U` iff every point `z ∈ U` has a punctured neighborhood that does not intersect
`U \ s`. -/
theorem codiscreteWithin_iff_locallyEmptyComplementWithin {s U : Set X} :
s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅ :=
by
simp only [mem_codiscreteWithin, disjoint_principal_right]
refine ⟨fun h z hz ↦ ⟨(U \ s)ᶜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩
rw [← exists_mem_subset_iff]
obtain ⟨t, h₁t, h₂t⟩ := h z hz
use t, h₁t, (disjoint_iff_inter_eq_empty.mpr h₂t).subset_compl_right
