ceil_sub_natCast — Mathlib

English

For a ∈ R and n ∈ ℕ, ⌈a − n⌉₊ = ⌈a⌉₊ − n.

Русский

Для a и n∈ℕ выполняется ⌈a − n⌉₊ = ⌈a⌉₊ − n.

LaTeX

$$$$ \\lceil a - n \\rceil_+ = \\lceil a \\rceil_+ - n $$$$

Lean4

@[simp]
theorem ceil_sub_natCast (a : R) (n : ℕ) : ⌈a - n⌉₊ = ⌈a⌉₊ - n :=
  by
  obtain han | hna := le_total a n
  · rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]
  · refine eq_tsub_of_add_eq ?_
    rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le hna)

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