funMap_sumInl — Mathlib

English

Equality of LHom.sumInl.sumElim with LHom.id on L.sum L'.

Русский

Равенство LHom.sumInl.sumElim LHom.sumInr и id на L.sum L'.

LaTeX

$$$LHom.sumInl.sumElim LHom.sumInr = LHom.id (L.sum L')$$$

Lean4

@[simp]
theorem funMap_sumInl [(L.sum L').Structure M] [(LHom.sumInl : L →ᴸ L.sum L').IsExpansionOn M] {n} {f : L.Functions n}
    {x : Fin n → M} : @funMap (L.sum L') M _ n (Sum.inl f) x = funMap f x :=
  (LHom.sumInl : L →ᴸ L.sum L').map_onFunction f x

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