instDenselyOrderedEReal — Mathlib

English

Between any two distinct elements of EReal there exists another element; i.e., EReal is densely ordered.

Русский

Между любыми двумя различными элементами EReal существует другой элемент; т. е. EReal образует плотно упорядоченную систему.

LaTeX

$$$ \forall a,b \in \mathrm{EReal},\ a < b \Rightarrow \exists c \in \mathrm{EReal},\ a < c \land c < b. $$$

Lean4

instance : DenselyOrdered EReal :=
  inferInstanceAs (DenselyOrdered (WithBot (WithTop ℝ)))

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