add_le_of_le

Mathlib.SetTheory.Cardinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.add_le_of_le

← MathLib Explorer

English

If c ≥ ℵ₀ and a ≤ c and b ≤ c, then a + b ≤ c.

Русский

Если c ≥ ℵ₀ и a ≤ c и b ≤ c, то a + b ≤ c.

LaTeX

$$$$(\aleph_0 \le c) \land (a \le c) \land (b \le c) \Rightarrow a + b \le c$$$$

Lean4

theorem add_le_of_le {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) : a + b ≤ c :=
  (add_le_add h1 h2).trans <| le_of_eq <| add_eq_self hc

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

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

Разделы

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

Аффилиация

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