A point-free look at Ostrowski's theorem and absolute values

Ming Ng, Steven Vickers

Code by ChatGPT, mostly.

theorem convention_1_7 (x y : ℝ) : x ≥ y ↔ ∀ (q : ℚ), x < ↑q → y < ↑q

From Convention 1.7.