truncGE'Map_comp — Mathlib

English

The truncGE'Map of a composition equals the composition of truncGE'Map's.

Русский

TruncGE'Map(c ∘ d) = TruncGE'Map(c) ∘ TruncGE'Map(d).

LaTeX

$$$truncGE'Map(\phi \;\,\;\,\phi') e = truncGE'Map(\phi,e) e \;\;\; truncGE'Map(\phi',e) e$$$

Lean4

@[reassoc, simp]
theorem truncGE'Map_comp : truncGE'Map (φ ≫ φ') e = truncGE'Map φ e ≫ truncGE'Map φ' e :=
  by
  ext i
  by_cases hi : e.BoundaryGE i
  · simp [truncGE'Map_f_eq_opcyclesMap _ _ hi rfl, opcyclesMap_comp]
  · simp [truncGE'Map_f_eq _ _ hi rfl]

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