toDenselyOrdered — Mathlib

English

In a densely ordered linear order with a semifield structure, between any two distinct points there is another point.

Русский

В плотно упорядоченном линейном порядке с полем-структурой между любыми двумя различными точками есть другая точка.

LaTeX

$$$\forall a,b\in \alpha\ (a

Lean4

instance (priority := 100) toDenselyOrdered : DenselyOrdered α where
  dense a₁ a₂
    h :=
    ⟨(a₁ + a₂) / 2,
      calc
        a₁ = (a₁ + a₁) / 2 := (add_self_div_two a₁).symm
        _ < (a₁ + a₂) / 2 := by gcongr; exact zero_lt_two,
      calc
        (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := by gcongr; exact zero_lt_two
        _ = a₂ := add_self_div_two a₂⟩

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