ceil_add_le

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.ceil_add_le

English

For a,b in the ring, ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊.

Русский

Для a,b в кольце справедливо ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊.

LaTeX

$$$$ \\lceil a + b \\rceil_+ \\le \\lceil a \\rceil_+ + \\lceil b \\rceil_+ $$$$

Lean4

@[bound]
theorem ceil_add_le (a b : R) : ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊ :=
  by
  rw [ceil_le, Nat.cast_add]
  gcongr <;> apply le_ceil

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

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

Разделы

Аффилиация

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