insert_mem_nhds_iff — Mathlib

English

Equivalent formulations for membership of insert a s in nhds a in terms of nhdsWithin.

Русский

Эквивалентные формулировки принадлежности insert a s фильтру Nhds a через nhdsWithin.

LaTeX

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

Lean4

theorem insert_mem_nhds_iff {a : α} {s : Set α} : insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a := by
  simp only [nhdsWithin, mem_inf_principal, mem_compl_iff, mem_singleton_iff, or_iff_not_imp_left, insert_def]

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