ne_top_iff_exists_not_inseparable

English

A topology t is not the top topology if and only if there exist x,y ∈ α with ¬Inseparable x y.

Русский

Топология t не равна верхней тогда и только тогда, существует пара точек x,y такие что ¬Inseparable x y.

LaTeX

$$$$ t \neq \top \iff \exists x,y \in \alpha, \neg Inseparable(x,y). $$$$

Lean4

theorem ne_top_iff_exists_not_inseparable {t : TopologicalSpace α} : t ≠ ⊤ ↔ ∃ x y : α, ¬Inseparable x y := by
  simpa using eq_top_iff_forall_inseparable.not

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