round_cast — Mathlib

English

For any x ∈ ℚ, ⌈x⌉_α = ⌈x⌉; i.e., casting to α preserves the ceiling.

Русский

Для любого x ∈ ℚ, ⌈x⌉_α = ⌈x⌉; т.е. округление вверх сохраняется при приведении к α.

LaTeX

$$$\lceil x \rceil_\alpha = \lceil x \rceil$$$

Lean4

@[simp, norm_cast]
theorem round_cast (x : ℚ) : round (x : α) = round x :=
  by
  have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
  rw [round_eq, round_eq, ← this, floor_cast]

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