sumMap_isExpansionOn — Mathlib

English

Another variant of SumElim compatibility with composition.

Русский

Другой вариант совместимости SumElim с композициями.

LaTeX

$$$\text{comp_sumElim }$$$

Lean4

instance sumMap_isExpansionOn {L₁ L₂ : Language} (ψ : L₁ →ᴸ L₂) (M : Type*) [L.Structure M] [L'.Structure M]
    [L₁.Structure M] [L₂.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M] : (ϕ.sumMap ψ).IsExpansionOn M :=
  ⟨fun f _ => Sum.casesOn f (by simp) (by simp), fun R _ => Sum.casesOn R (by simp) (by simp)⟩

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