isZero_extend_X — Mathlib

English

Let K extendable along e be a homological complex. If every preimage index i maps to a distinct i' ≠ e.f i, then the X-component at i' is zero.

Русский

Пусть K можно расширить вдоль e; если для каждого i верно, что e.f i ≠ i', тогда X-компонента по i' равна нулю.

LaTeX

$$$\\forall i',\\; (\\forall i, e.f(i) \\neq i') \\Rightarrow (K\\extend e)\\,X\\,i' \\cong 0$$$

Lean4

theorem isZero_extend_X (i' : ι') (hi' : ∀ i, e.f i ≠ i') : IsZero ((K.extend e).X i') :=
  K.isZero_extend_X' e i' (ComplexShape.Embedding.r_eq_none e i' hi')

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