restrictionToTruncGE'_f_eq_iso_hom_iso_inv

English

For i and i' with hi', hi, the f-component equals restrictionXIso.hom composed with inv of truncGE'XIso.

Русский

Для i, i' с hi', hi f-компонента равна restrictionXIso.hom ∘ (truncGE'XIso).inv.

LaTeX

$$$(K.restrictionToTruncGE' e).f i = (K.restrictionXIso e hi').hom \circ (K.truncGE'XIso e hi' hi).inv$$$

Lean4

theorem restrictionToTruncGE'_f_eq_iso_hom_iso_inv {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i) :
    (K.restrictionToTruncGE' e).f i = (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv := by
  apply restrictionToTruncGE'.f_eq_iso_hom_iso_inv

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