sumElim_isExpansionOn — Mathlib

English

SumElim preserves the expansion-on property under suitable assumptions.

Русский

SumElim сохраняет свойство расширения при надлежащих предпосылках.

LaTeX

$$$(\varphi.sumElim \psi).IsExpansionOn M$$$

Lean4

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

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