mem_nhdsWithin_of_mem_nhds — Mathlib

English

If s is a neighborhood of a in the ambient space, then s is a neighborhood of a in any nhdsWithin a t.

Русский

Если s является окрестностью a в глобальном пространстве, то она является окрестностью a и в nhdsWithin a t.

LaTeX

$$$ s \in \mathcal{N}(a) \Rightarrow s \in \mathcal{N}_t(a) $$$

Lean4

theorem mem_nhdsWithin_of_mem_nhds {s t : Set α} {a : α} (h : s ∈ 𝓝 a) : s ∈ 𝓝[t] a :=
  mem_inf_of_left h

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