English
The maps toNNRat and the inclusion form a Galois insertion; equivalently, for p ∈ ℚ≥0 and r ∈ ℚ, toNNRat(p) ≤ r iff p ≤ (r : ℚ≥0).
Русский
Отображения toNNRat и включение образуют Галуа-инсерцию; эквивалентно, для p ∈ ℚ≥0 и r ∈ ℚ, toNNRat(p) ≤ r тогда и только тогда, p ≤ (r : ℚ≥0).
LaTeX
$$$$ \forall p \in \mathbb{Q}_{\ge 0}, \forall r \in \mathbb{Q}, \ \mathrm{toNNRat}(p) \le r \iff p \le (r : \mathbb{Q}_{\ge 0}). $$$$
Lean4
/-- `toNNRat` and `(↑) : ℚ≥0 → ℚ` form a Galois insertion. -/
protected def gi : GaloisInsertion toNNRat (↑) :=
GaloisInsertion.monotoneIntro coe_mono toNNRat_mono Rat.le_coe_toNNRat toNNRat_coe
