inseparable_top — Mathlib

English

In the trivial topology, any two points are inseparable: for all x,y ∈ α, Inseparable x y.

Русский

В тривиальной топологии любые две точки неразделимы: для любых x,y ∈ α выполняется Inseparable x y.

LaTeX

$$$$ \forall x,y \in \alpha, \ Inseparable(x,y). $$$$

Lean4

/-- In the trivial topology no points are separable.

The corresponding `bot` lemma is handled more generally by `inseparable_iff_eq`. -/
@[simp]
theorem inseparable_top (x y : α) : @Inseparable α ⊤ x y :=
  nhds_top.trans nhds_top.symm

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