le_add_left

Mathlib.Computability.Reduce

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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