isOpen_singleton_nhdsAdjoint — Mathlib

English

In the nhdsAdjoint topology, every singleton {b} with b ≠ a is open.

Русский

В топологии nhdsAdjoint каждый синглтон {b} при b ≠ a открыто.

LaTeX

$$theorem isOpen_singleton_nhdsAdjoint {α : Type u} {a b : α} (f : Filter α) (hb : b ≠ a) : IsOpen[nhdsAdjoint a f] { b }$$

Lean4

theorem isOpen_singleton_nhdsAdjoint {α : Type*} {a b : α} (f : Filter α) (hb : b ≠ a) :
    IsOpen[nhdsAdjoint a f] { b } := fun h ↦ absurd h hb.symm

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