inseparableSetoid_eq_top_iff — Mathlib

English

For α with topology t, inseparableSetoid α = ⊤ if and only if t = ⊤ (the indiscrete topology).

Русский

Для α с топологией t равенство inseparableSetoid α = ⊤ происходит тогда и только тогда, когда t = ⊤ (индицентрическая топология).

LaTeX

$$$\\inseparableSetoid(α) = \\top \\;\\iff\\; t = \\top$$$

Lean4

@[simp]
theorem inseparableSetoid_eq_top_iff {t : TopologicalSpace α} : inseparableSetoid α = ⊤ ↔ t = ⊤ :=
  Setoid.eq_top_iff.trans TopologicalSpace.eq_top_iff_forall_inseparable.symm

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