isStrictlyGE_shift — Mathlib

English

If K isGE at n, then shifting K by a preserves GE, i.e., (K⟦a⟧) isGE at n' when a+n' = n.

Русский

Если K GE в n, то сдвиг K на a сохраняет GE: (K⟦a⟧) имеет GE в n' при условии a+n' = n.

LaTeX

$$$ (n) [K.IsGE(n)] (a, n') \\, (h: a+n' = n) \\Rightarrow (K\\lceil a \\rceil).IsGE(n') $$$

Lean4

theorem isStrictlyGE_shift (n : ℤ) [K.IsStrictlyGE n] (a n' : ℤ) (h : a + n' = n) : (K⟦a⟧).IsStrictlyGE n' :=
  by
  rw [isStrictlyGE_iff]
  intro i hi
  exact IsZero.of_iso (K.isZero_of_isStrictlyGE n _ (by cutsat)) (K.shiftFunctorObjXIso a i _ rfl)

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