nhds_ne_subtype_neBot_iff — Mathlib

English

Let S ⊆ X and x ∈ S. The nontrivial nhds on S at x is nontrivial iff the nontrivial nhds on X at x, intersected with 𝓟S, is nontrivial.

Русский

Пусть S ⊆ X и x ∈ S. Непустой фильтр окрестностей на подмножестве S в точке x эквивалентен непустому фильтру окрестностей в X, пересечённому с 𝓟S.

LaTeX

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

Lean4

theorem nhds_ne_subtype_neBot_iff {S : Set X} {x : S} : (𝓝[≠] x).NeBot ↔ (𝓝[≠] (x : X) ⊓ 𝓟 S).NeBot := by
  rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]

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