nhds_of_nhdsWithin_of_nhds — Mathlib

English

In a topological space, if s is a neighborhood of a and t is a neighborhood of a within s, then t is a neighborhood of a.

Русский

В топологическом пространстве, если s является окрестностью точки a, а t является окрестностью a внутри s, то t является окрестностью a.

LaTeX

$$$ s \in \mathcal{N}(a) \land t \in \mathcal{N}_s(a) \Rightarrow t \in \mathcal{N}(a) $$$

Lean4

theorem nhds_of_nhdsWithin_of_nhds {s t : Set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ 𝓝[s] a) : t ∈ 𝓝 a :=
  by
  rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩
  exact (𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

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