extendMap_comp — Mathlib

English

The extension of a composition equals the composition of extensions: extendMap (φ ≫ φ') e = extendMap φ e ≫ extendMap φ' e.

Русский

Расширение композиции равно композиции расширений: extendMap (φ ≫ φ') e = extendMap φ e ≫ extendMap φ' e.

LaTeX

$$$\\text{extendMap} (\\phi \\circ \\phi')\, e = \\text{extendMap} \\phi\, e \\circ \\text{extendMap} \\phi'\\, e$$$

Lean4

@[reassoc, simp]
theorem extendMap_comp : extendMap (φ ≫ φ') e = extendMap φ e ≫ extendMap φ' e :=
  by
  ext i'
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]
  · simp [extendMap_f_eq_zero _ e i' (fun i hi => hi' ⟨i, hi⟩)]

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