elim_one_mulSingle — Mathlib

English

Let i ∈ β, c ∈ γ. Then Sum.elim (1 : α → γ) (Pi.mulSingle i c) equals Pi.mulSingle (Sum.inr i) c.

Русский

Пусть i ∈ β, c ∈ γ. Тогда Sum.elim (1 : α → γ) (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c.

LaTeX

$$$ \text{Sum.elim } (1 : \alpha \to \gamma) (\Pi.mulSingle i c) = \Pi.mulSingle (\text{Sum.inr } i) c $$$

Lean4

@[to_additive (attr := simp)]
theorem elim_one_mulSingle [DecidableEq α] [DecidableEq β] [One γ] (i : β) (c : γ) :
    Sum.elim (1 : α → γ) (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c := by
  simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]

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