extend_exactAt — Mathlib

English

Exactness at j in K extends to exactness at j' in K.extend e, provided that e matches the indices suitably.

Русский

Точность в позиции j в K переходит в точность в позиции j' в K.extend e при надлежащем соответствии индексов.

LaTeX

$$ExtendExactAt (K) e (j')$$

Lean4

theorem extend_exactAt (j' : ι') (hj' : ∀ j, e.f j ≠ j') : (K.extend e).ExactAt j' :=
  exactAt_of_isSupported _ e j' hj'

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