instDenselyOrderedSubtypeReal — Mathlib

English

Irrationals are densely ordered: between any two irrational numbers there exists another irrational.

Русский

Иррациональные числа плотно упорядочены: между любыми двумя иррациональными числами существует другая иррациональная.

LaTeX

$$$\forall a,b\in\mathbb{R},\ a

Lean4

instance : DenselyOrdered { x // Irrational x } :=
  ⟨fun _ _ hlt =>
    let ⟨z, hz, hxz, hzy⟩ := exists_irrational_btwn hlt
    ⟨⟨z, hz⟩, hxz, hzy⟩⟩

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