sumElim_comp_relabelAux — Mathlib

English

The composition of sum-elimination with relabelAux equals a explicit sum-elimination with a transformed indexing.

Русский

Составление Sum.elim с relabelAux эквивалентно явному Sum.elim с преобразованной индексацией.

LaTeX

$$$Sum.elim v xs \circ relabelAux g m = Sum.elim (Sum.elim v (xs \circ castAdd m) \circ g) (xs \circ natAdd n).$$$

Lean4

@[simp]
theorem sumElim_comp_relabelAux {m : ℕ} {g : α → β ⊕ (Fin n)} {v : β → M} {xs : Fin (n + m) → M} :
    Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) :=
  by
  ext x
  rcases x with x | x
  · simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]
    rcases g x with l | r <;> simp
  · simp [BoundedFormula.relabelAux]

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