coe_ceil — Mathlib

English

The floor of x when viewed in any ambient field K with a compatible order equals the floor of x in the nonnegative rationals.

Русский

Пол числа x, представленного в произвольном окружении K с совместимым порядком, равен floor(x) в ℚ≥0.

LaTeX

$$∀ {K} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K], (x ∈ ℚ_{≥0}) ⇒ ⌊x\!\uparrow_K⌋_{+} = ⌊x⌋_{+}$$

Lean4

@[simp, norm_cast]
theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ :=
  Int.natCast_ceil_eq_ceil q.coe_nonneg

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