diff_empty — Mathlib

English

If s is a topological basis, then removing the empty set from s yields a topological basis.

Русский

Если s является базой, удаление пустого множества из s образует базу.

LaTeX

$$diff_empty {s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (s \\ {∅})$$

Lean4

theorem diff_empty {s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (s \ {∅}) :=
  isTopologicalBasis_of_isOpen_of_nhds (fun _ hu ↦ h.isOpen hu.1) fun a _ ha hu ↦
    have ⟨t, hts, ht⟩ := h.isOpen_iff.mp hu a ha
    ⟨t, ⟨hts, ne_of_mem_of_not_mem' ht.1 <| notMem_empty _⟩, ht⟩

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