English
Let X be a topological space, S and T be subsets of X, and x an element of S. The neighborhood filter of x in the subspace S, corresponding to T via the inclusion map, is the bottom filter if and only if the neighborhood filter of x in T, when intersected with the principal filter on S, is the bottom filter. Equivalently, 𝓝[((↑) : S → X) ⁻¹' T] x = ⊥ if and only if 𝓝[T] (x) ⊓ 𝓟 S = ⊥.
Русский
Пусть X — топологическое множество, S ⊆ X, T ⊆ X, и x ∈ S. Фильтр окрестностей x в подпространстве S, образующийся при включении i: S → X и взорвавшемся на T, равен нулевому фильтру тогда и только тогда, когда фильтр окрестностей x в T, пересечённый с фильтром-основанием 𝓟S, равен нулю. Эквивалентно: 𝓝[((↑):S→X]⁻¹' T] x = ⊥ ⇔ 𝓝[T](x) ⊓ 𝓟S = ⊥.
LaTeX
$$$$\\mathcal N_{((\\uparrow):S\\to X)^{-1} T}(x) = \\bot \\;\\Longleftrightarrow\\; \\mathcal N_T(x) \\sqcap \\mathcal P(S) = \\bot.$$$$
Lean4
theorem nhdsWithin_subtype_eq_bot_iff {s t : Set X} {x : s} : 𝓝[((↑) : s → X) ⁻¹' t] x = ⊥ ↔ 𝓝[t] (x : X) ⊓ 𝓟 s = ⊥ :=
by rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal, nhds_induced]
