English
The nonnegative part of α inherits a FloorSemiring structure, with floor and ceil coming from α via the inclusion.
Русский
Неотрицательная часть α наследует структуру FloorSemiring, где floor и ceil берутся по α через вложение.
LaTeX
$$$\\text{FloorSemiring}({x : α // 0 ≤ x})$ with $\\text{floor}(a) = \\lfloor a \\rfloor_+, \\; \\text{ceil}(a) = \\lceil a \\rceil_+$$$
Lean4
instance floorSemiring [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] :
FloorSemiring { r : α // 0 ≤ r } where
floor a := ⌊(a : α)⌋₊
ceil a := ⌈(a : α)⌉₊
floor_of_neg ha := FloorSemiring.floor_of_neg ha
gc_floor ha := FloorSemiring.gc_floor (Subtype.coe_le_coe.2 ha)
gc_ceil a n := FloorSemiring.gc_ceil (a : α) n
