mem_codiscreteWithin_accPt — Mathlib

English

A set S belongs to codiscreteWithin(T) iff for every x ∈ T, no accumulation point of T\S lies in the principal of S.

Русский

S ∈ codiscreteWithin(T) эквивалентно тому, что для каждого x ∈ T точка не является накоплением множества T\\S в отношении к S.

LaTeX

$$$S ∈ codiscreteWithin(T) \\iff \\forall x ∈ T, Not(AccPt x (\\operatorname{principal}(T\\setminus S)))$$$

Lean4

theorem mem_codiscreteWithin_accPt {S T : Set X} : S ∈ codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (𝓟 (T \ S)) := by
  simp only [mem_codiscreteWithin, disjoint_iff, AccPt, not_neBot]

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