intCeil_cast — Mathlib

English

For x ∈ ℚ≥0, the integer ceiling of x in K equals the integer ceiling of x in ℚ≥0.

Русский

Для x ∈ ℚ≥0 целая часть округления вверх x в K равна целой части округления вверх x в ℚ≥0.

LaTeX

$$Int.ceil x.cast = Int.ceil x.cast$$

Lean4

@[simp, norm_cast]
theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉ :=
  by
  rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
  constructor
  · have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x
    rw [NNRat.cast_add, NNRat.cast_one] at this
    refine Eq.trans_lt ?_ this
    norm_cast
  · rw [Int.cast_natCast, NNRat.cast_le_natCast]
    exact Nat.le_ceil _

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