σ_comp_PInfty — Mathlib

English

For each i in Fin(n+1), X.σ i commutes with PInfty.f(n+1) to give zero: X.σ i ≫ PInfty.f(n+1) = 0.

Русский

Для каждого i в Fin(n+1) композиция X.σ i с PInfty.f(n+1) равна нулю: X.σ i ≫ PInfty.f(n+1) = 0.

LaTeX

$$$$ X.\\sigma(i) \\circ PInfty.f(n+1) = 0. $$$$

Lean4

@[reassoc (attr := simp)]
theorem σ_comp_PInfty (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) : X.σ i ≫ PInfty.f (n + 1) = 0 :=
  by
  rw [PInfty_f, σ_comp_P_eq_zero X i]
  simp only [le_add_iff_nonneg_left, zero_le]

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