ceil_cast — Mathlib

English

The ceiling of x in K matches the ceiling of x in ℚ≥0 after coercion.

Русский

Округление вверх x в K совпадает с округлением вверх x в ℚ≥0 после приведения.

LaTeX

$$⌈x⌉_{K} = ⌈x⌉_{ℚ≥0}$$

Lean4

@[simp, norm_cast]
theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · simp
  · refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa

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