floor_add_ofNat — Mathlib

English

For a ∈ R and n ∈ ℕ with n ≥ 2, ⌊a + ofNat(n)⌋ = ⌊a⌋ + ofNat(n).

Русский

Для a ∈ R и n ∈ ℕ с n ≥ 2 верно ⌊a + ofNat(n)⌋ = ⌊a⌋ + ofNat(n).

LaTeX

$$$$\forall a \in R,\forall n \in \mathbb{N},\ [n \ge 2] \Rightarrow \left\lfloor a + \mathrm{ofNat}(n) \right\rfloor = \left\lfloor a \right\rfloor + \mathrm{ofNat}(n).$$$$

Lean4

@[simp]
theorem floor_add_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a + ofNat(n)⌋ = ⌊a⌋ + ofNat(n) :=
  floor_add_natCast a n

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