nhdsWithin_restrict'' — Mathlib

English

If t ∈ 𝓝[s] a, then 𝓝[s] a = 𝓝[s ∩ t] a.

Русский

Если t является окрестностью внутри s точки a, то 𝓝[s] a = 𝓝[s ∩ t] a.

LaTeX

$$$ \mathcal{N}_s(a) = \mathcal{N}_{s \cap t}(a) $$$

Lean4

theorem nhdsWithin_restrict'' {a : α} (s : Set α) {t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s] a = 𝓝[s ∩ t] a :=
  le_antisymm (le_inf inf_le_left (le_principal_iff.mpr (inter_mem self_mem_nhdsWithin h)))
    (inf_le_inf_left _ (principal_mono.mpr Set.inter_subset_left))

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