insert_mem_nhdsWithin_insert — Mathlib

English

An insert a s belongs to nhds a if and only if s belongs to nhds within ≠ a.

Русский

Прибавление a к s принадлежит nhds a тогда и только тогда, когда s принадлежит nhdsWithin a с исключением a.

LaTeX

$$$$ insert(a,s) \\in 𝓝(a) \\iff s \\in 𝓝[\\neq] a $$$$

Lean4

theorem insert_mem_nhdsWithin_insert {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : insert a t ∈ 𝓝[insert a s] a := by
  simp [mem_of_superset h]

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