floor_coe — Mathlib

English

The natural floor of q, when viewed as a rational, equals the floor of q considered in the nonnegative rationals. In formula: ⌊q⌋₊ = ⌊q⌋ (as a natural number).

Русский

Целая часть q, взятая как элемент ℚ≥0, совпадает с целой part q как неотрицательного рационального числа: ⌊q⌋₊ = ⌊q⌋.

LaTeX

$$∀ q ∈ ℚ≥0, ⌊q⌋_{+} = ⌊q⌋$$

Lean4

@[simp, norm_cast]
theorem floor_coe (q : ℚ≥0) : ⌊(q : ℚ)⌋₊ = ⌊q⌋₊ :=
  rfl

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