le_add_congr

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.le_add_congr

English

If l1 ≤ m1 and l2 ≤ m2, then l1 + l2 ≤ m1 + m2.

Русский

Если l1 ⊆ m1 и l2 ⊆ m2, то l1 + l2 ⊆ m1 + m2.

LaTeX

$$$ l_1 \le m_1 \to l_2 \le m_2 \to l_1 + l_2 \le m_1 + m_2 $$$

Lean4

theorem le_add_congr {l₁ l₂ m₁ m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂ :=
  sup_le_sup

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

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

Разделы

Аффилиация

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