comp_sumElim — Mathlib

English

The composition with sumElim is compatible with LHom composition.

Русский

Сочетание с sumElim совместимо с обычной композицией LHom.

LaTeX

$$$\theta.comp(\varphi.sumElim \psi) = (\theta.comp \varphi).sumElim (\theta.comp \psi)$$$

Lean4

theorem comp_sumElim {L3 : Language} (θ : L' →ᴸ L3) : θ ∘ᴸ ϕ.sumElim ψ = (θ ∘ᴸ ϕ).sumElim (θ ∘ᴸ ψ) :=
  LHom.funext (funext fun _n => Sum.comp_elim _ _ _) (funext fun _n => Sum.comp_elim _ _ _)

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