ceil_def' — Mathlib

English

For any q ∈ ℚ, the ceiling equals the negative floor of the negation expression: ⌈q⌉ = -(-q.num / q.den).

Русский

Для любого q ∈ ℚ крышка равна −(−q.num / q.den).

LaTeX

$$$\lceil q \rceil = -\left(-\dfrac{q.num}{q.den}\right)$$$

Lean4

/-- This variant of `ceil_def` uses the `Int.ceil` (for any `FloorRing`) rather than `Rat.ceil`.
-/
protected theorem ceil_def' (q : ℚ) : ⌈q⌉ = -(-q.num / ↑q.den) :=
  by
  change -⌊-q⌋ = _
  rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]

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