nhdsWithin_inter — Mathlib

English

The neighborhood at a from the intersection s ∩ t equals the infimum of the neighborhood filters within s and within t.

Русский

Окрестность в a от пересечения s ∩ t равна наименьшему (infimum) из 𝓝[s] a и 𝓝[t] a.

LaTeX

$$$$ 𝓝[s \\cap t](a) = 𝓝[s](a) \\wedge 𝓝[t](a) $$$$

Lean4

theorem nhdsWithin_inter (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a :=
  by
  delta nhdsWithin
  rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]

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