exactAt_of_isSupported — Mathlib

English

If K is supported with respect to e, then for every i' with no i mapping to i' under e, K has exactness at i'.

Русский

Если K поддержан относительно вложения e, то для каждого i' с условием, что не существует i such that e.f(i) = i', комплекс K имеет точность в позиции i'.

LaTeX

$$$K.IsSupported(e) \Rightarrow \forall i' \bigl( (\forall i, e.f(i) \neq i') \Rightarrow K.ExactAt(i') \bigr)$$$

Lean4

theorem exactAt_of_isSupported [K.IsSupported e] (i' : ι') (hi' : ∀ i, e.f i ≠ i') : K.ExactAt i' :=
  IsSupported.exactAt i' hi'

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