add_left

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.Raised.add_left

English

Adding a fixed offset k preserves Raised: if n ≤ m then (k+n) ≤ (k+m) or (k+n) = (k+m) or (k+m) = k+n+1 based on the original relation.

Русский

Прибавление константы сохраняет Raised: Raised n m → Raised (k+n) (k+m).

LaTeX

$$Raised(n,m) → Raised(k+n,k+m)$$

Lean4

theorem add_left (k) {n m} (H : Raised n m) : Raised (k + n) (k + m) :=
  by
  rcases H with (rfl | rfl)
  · exact Or.inl rfl
  · exact Or.inr rfl

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

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

Разделы

Аффилиация

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