add_div_le_add_div

Mathlib.Data.Nat.ModEq

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

← MathLib Explorer

English

For natural numbers a,b,c, a/c + b/c ≤ (a+b)/c.

Русский

Для натуральных a,b,c верно a/c + b/c ≤ (a+b)/c.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\mathbb{N},\\\\ a/c + b/c \\\\le (a+b)/c$$$

Lean4

theorem add_div_le_add_div (a b c : ℕ) : a / c + b / c ≤ (a + b) / c :=
  if hc0 : c = 0 then by simp [hc0] else by rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]; exact Nat.le_add_right _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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