toFloorSemiring — Mathlib

English

The nat representation of the floor equals the Nat-floor of a: ⌊a⌋.toNat = ⌊a⌋₊.

Русский

Число Nat, получаемое из ⌊a⌋, равно Nat-представлению ⌊a⌋: ⌊a⌋.toNat = ⌊a⌋₊.

LaTeX

$$$\lfloor a \rfloor.toNat = \lfloor a \rfloor_+.$$$

Lean4

instance (priority := 100) toFloorSemiring : FloorSemiring α
    where
  floor a := ⌊a⌋.toNat
  ceil a := ⌈a⌉.toNat
  floor_of_neg {_} ha := Int.toNat_of_nonpos (Int.floor_nonpos ha.le)
  gc_floor {a n} ha := by rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]
  gc_ceil a n := by rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]

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