le_add_right

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#ManyOneDegree.le_add_right

English

For any d1, d2 in the degree structure, d2 ≤ d1 + d2.

Русский

Для любых степеней d1, d2 выполняется d2 ≤ d1 + d2.

LaTeX

$$$$ d_2 \\le d_1 + d_2. $$$$

Lean4

@[simp]
protected theorem le_add_right (d₁ d₂ : ManyOneDegree) : d₂ ≤ d₁ + d₂ :=
  (ManyOneDegree.add_le.1 (le_refl _)).2

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

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

Разделы

Аффилиация

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