nhdsWithin_inter' — Mathlib

English

The neighborhood at a from the intersection s ∩ t equals the infimum of 𝓝[s] a and the principal filter of t.

Русский

Окрестность в a от пересечения s ∩ t равна пересечению 𝓝[s] a и 𝓟 t.

LaTeX

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

Lean4

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

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