δ_inl — Mathlib

English

Statement about extensionality of cochains from X_j by inl/inr; equivalent to ext_from_iff in a shifted form.

Русский

Утверждение об эксенциальности коцепей через inl/inr; эквивалентно ext_from_iff в смещенной форме.

LaTeX

$$$\forall i,j:\ hij: j+1=i:\ γ_1,γ_2:\ Cochain (mappingCone φ) X_j K i:\ (γ_1=γ_2) \iff (inl φ)_{i,j}∘γ_1 = (inl φ)_{i,j}∘γ_2 \land (inr φ)∘γ_1 = (inr φ)∘γ_2.$$$

Lean4

@[simp]
theorem δ_inl : δ (-1) 0 (inl φ) = Cochain.ofHom (φ ≫ inr φ) :=
  by
  ext p
  simp [δ_v (-1) 0 (neg_add_cancel 1) (inl φ) p p (add_zero p) _ _ rfl rfl,
    inl_v_d φ p (p - 1) (p + 1) (by cutsat) (by cutsat)]

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