eq_top_iff_forall_inseparable — Mathlib

English

For a topology t on α, t = ⊤ if and only if every pair of points is inseparable.

Русский

Для топологии t на α: t = ⊤ тогда и только тогда, когда каждая пара точек неразделима.

LaTeX

$$$$ t = \top \ \Longleftrightarrow \ \forall x,y \in \alpha, \ Inseparable(x,y). $$$$

Lean4

theorem eq_top_iff_forall_inseparable {t : TopologicalSpace α} : t = ⊤ ↔ (∀ x y : α, Inseparable x y)
    where
  mp h := h ▸ inseparable_top
  mpr h := ext_nhds fun x => nhds_top ▸ top_unique fun _ hs a => mem_of_mem_nhds <| h x a ▸ hs

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