discreteTopology_subtype_iff — Mathlib

English

A subspace S of X is discrete iff for every x in S, the intersection of the nontrivial neighborhood filter at x with 𝓟S is the bottom filter.

Русский

Подпространство S в X дискретно тогда и только тогда для каждого x∈S пересечение ненулевого фильтра окрестностей x с 𝓟S равно ⊥.

LaTeX

$$$$ DiscreteTopology(S) \\iff \\forall x\\in S,\\quad \\mathcal N^{\\neq}_S(x) \\sqcap \\mathcal P(S) = \\bot. $$$$

Lean4

theorem discreteTopology_subtype_iff {S : Set X} : DiscreteTopology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥ := by
  simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]

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