English
S belongs to codiscreteWithin(T) iff S is a member of the codiscreteWithin filter on T; equivalently, the membership is characterized by the clause using disjointness with principal of T\\S.
Русский
S ∈ codiscreteWithin(T) тогда и только тогда, когда S является элементом фильтра codiscreteWithin(T), эквивалентно описанию через Disjoint и principal(T\\S).
LaTeX
$$$S ∈ \\operatorname{codiscreteWithin}(T) \\iff \\forall x, x ∈ T \\Rightarrow Disjoint(\\mathcal{N}_{x}^{\\neq}) (\\mathcal{P}(T \\setminus S))$$$
Lean4
theorem mem_codiscreteWithin {S T : Set X} : S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S)) :=
by
simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def, mem_diff, mem_inter_iff,
mem_compl_iff]
congr! 7 with x - u y
tauto
