nat_floor_coe — Mathlib

English

The natural-number floor of a nonnegative element equals the floor taken in α.

Русский

Целочисленный пол floor элемента неотрицательного совпадает с floor в α.

LaTeX

$$$\\mathrm{Nat}.\\mathrm{floor}(a) = \\mathrm{Nat}.\\mathrm{floor}(a_{\\alpha})$$$

Lean4

@[norm_cast]
theorem nat_floor_coe [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
    ⌊(a : α)⌋₊ = ⌊a⌋₊ :=
  rfl

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