floor_ofNat_add — Mathlib

English

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

Русский

Для a ∈ R и n ∈ ℕ с n ≥ 2: ⌊ofNat(n) + a⌋ = ofNat(n) + ⌊a⌋.

LaTeX

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

Lean4

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

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