mem_codiscreteWithin_iff_forall_mem_nhdsNE

English

A set S lies in codiscreteWithin(T) iff for every x ∈ T, S ∪ T^c is a punctured neighborhood of x.

Русский

S лежит в codiscreteWithin(T) тогда и только тогда, когда для каждого x ∈ T множество S ∪ T^c является пунктированной окрестностью x.

LaTeX

$$$S ∈ codiscreteWithin(T) \\iff \\forall x ∈ T, S \\cup T^c ∈ \\mathcal{N}_{x}^{\\neq}$$$

Lean4

/-- A set `s` is codiscrete within `U` iff `s ∪ Uᶜ` is a punctured neighborhood of every point in `U`.
-/
theorem mem_codiscreteWithin_iff_forall_mem_nhdsNE {S T : Set X} : S ∈ codiscreteWithin T ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x :=
  by simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff]

Похожие утверждения