nhds_ne_subtype_eq_bot_iff — Mathlib

English

Let S be a subset of a space X and x ∈ S. The nhds with the all-neighborhoods-excluding x in S equals ⊥ if and only if the nhds excluding x in X, restricted to S, is ⊥. In symbols, 𝓝[≠] S (x) = ⊥ iff 𝓝[≠] X (x) ⊓ 𝓟 S = ⊥.

Русский

Пусть S ⊆ X и x ∈ S. Наблюдательные фильтры 𝓝[≠]_S(x) равен ⊥ тогда и только тогда, когда 𝓝[≠]_X(x) ⊓ 𝓟S = ⊥.

LaTeX

$$$$\\mathcal N^{\\neq}_S(x) = \\bot \\iff \\mathcal N^{\\neq}_X(x) \\sqcap \\mathcal P(S) = \\bot.$$$$

Lean4

theorem nhds_ne_subtype_eq_bot_iff {S : Set X} {x : S} : 𝓝[≠] x = ⊥ ↔ 𝓝[≠] (x : X) ⊓ 𝓟 S = ⊥ := by
  rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton, Subtype.coe_injective.preimage_image]

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