floor_natCast_add

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.floor_natCast_add

English

For any n ∈ ℕ and a ∈ R: ⌊n + a⌋ = n + ⌊a⌋.

Русский

Для любого n ∈ ℕ и a ∈ R: ⌊n + a⌋ = n + ⌊a⌋.

LaTeX

$$$$\forall n \in \mathbb{N},\ a \in R:\ \left\lfloor n + a \right\rfloor = n + \left\lfloor a \right\rfloor.$$$$

Lean4

@[simp]
theorem floor_natCast_add (n : ℕ) (a : R) : ⌊↑n + a⌋ = n + ⌊a⌋ := by rw [← Int.cast_natCast, floor_intCast_add]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru