comp_δ_eq_zero — Mathlib

English

From v, for j ≠ 0 with appropriate bound, φ ≫ X.δ_j = 0.

Русский

Из v следует: для j ≠ 0 и подходящего предела, φ ≫ X.δ_j = 0.

LaTeX

$$$$ φ \\circ X.δ_j = 0 \\quad\\text{for } j \\neq 0 \\text{ and } n+2 \\le (j:\\mathbb{N}) + q. $$$$

Lean4

@[reassoc]
theorem comp_δ_eq_zero {Y : C} {n : ℕ} {q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) (j : Fin (n + 2))
    (hj₁ : j ≠ 0) (hj₂ : n + 2 ≤ (j : ℕ) + q) : φ ≫ X.δ j = 0 :=
  by
  obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero hj₁
  apply v i
  simp only [Fin.val_succ] at hj₂
  cutsat

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