shift_ge — Mathlib

English

Shift of le isomorphically equal: (t.le n).shift a = t.le (n+a).

Русский

Сдвиг левостороннего уровня имеет изоморфизм: (t.le n).shift a = t.le (n+a).

LaTeX

$$$(t.le\\ n).shift a = t.le (n+a)$$$

Lean4

theorem shift_ge (a n n' : ℤ) (hn' : a + n = n') : (t.ge n).shift a = t.ge n' :=
  by
  ext X
  constructor
  · intro hX
    exact ((t.ge n').prop_iff_of_iso ((shiftEquiv C a).unitIso.symm.app X)).1 (t.ge_shift n (-a) n' (by cutsat) _ hX)
  · intro hX
    exact t.ge_shift _ _ _ hn' X hX

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