ceil_add_natCast — Mathlib

English

For ha ≥ 0 and n ∈ ℕ, ⌈a + n⌉₊ = ⌈a⌉₊ + n.

Русский

Пусть a ≥ 0 и n ∈ ℕ. Тогда ⌈a + n⌉₊ = ⌈a⌉₊ + n.

LaTeX

$$$$ \\lceil a + \\operatorname{ofNat}(n) \\rceil_+ = \\lceil a \\rceil_+ + \\operatorname{ofNat}(n) $$$$

Lean4

theorem ceil_add_natCast (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
  eq_of_forall_ge_iff fun b => by
    rw [← not_lt, ← not_lt, not_iff_not, lt_ceil]
    obtain hb | hb := le_or_gt n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right, lt_ceil]
    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

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