floor_neg

Mathlib.Algebra.Order.Floor.Ring

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

English

For any a in R, floor(-a) = -ceil(a).

Русский

Для любого a ∈ R, floor(−a) = −ceil(a).

LaTeX

$$$\\\\lfloor -a \\\\rfloor = -\\\\lceil a \\\\rceil$$$

Lean4

theorem floor_neg : ⌊-a⌋ = -⌈a⌉ :=
  eq_of_forall_le_iff fun z => by rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]

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

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

Разделы

Аффилиация

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