English
The nonnegative rationals ℚ≥0 carry a FloorSemiring structure, where floor and ceil are defined by the usual floor/ceil of the underlying real values: floor q = ⌊q.val⌋₊ and ceil q = ⌈q.val⌉₊.
Русский
Неотрицательные рациональные числа ℚ≥0 образуют структуру FloorSemiring, где floor и ceil задаются как обычные floor/ceil для действительных значений: floor q = ⌊q.val⌋₊, ceil q = ⌈q.val⌉₊.
LaTeX
$$\text{there is a FloorSemiring structure on }\mathbb{Q}_{\ge 0} \text{ with } \text{floor}(q) = \lfloor q\rfloor_{\mathbb{N}}, \ \text{ceil}(q) = \lceil q\rceil_{\mathbb{N}}.$$
Lean4
instance : FloorSemiring ℚ≥0 where
floor q := ⌊q.val⌋₊
ceil q := ⌈q.val⌉₊
floor_of_neg h := by simpa using h.trans zero_lt_one
gc_floor {a n} h := by rw [← NNRat.coe_le_coe, Nat.le_floor_iff] <;> norm_cast
gc_ceil {a b} := by rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast
