nhdsWithin_inter_of_mem — Mathlib

English

If s is a neighborhood of a within t, then the intersection s ∩ t has the same neighborhood as t.

Русский

Если s является окрестностью a внутри t, то s ∩ t имеет ту же окрестность, что и t.

LaTeX

$$$$ 𝓝[a]_{[s \\cap t]} = 𝓝[t](a) $$$$

Lean4

theorem nhdsWithin_inter_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : 𝓝[s ∩ t] a = 𝓝[t] a :=
  by
  rw [nhdsWithin_inter, inf_eq_right]
  exact nhdsWithin_le_of_mem h

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