elim_mulSingle_one — Mathlib

English

Let i be in α, c in γ. Then Sum.elim (Pi.mulSingle i c) (1 : β → γ) equals Pi.mulSingle (Sum.inl i) c.

Русский

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

LaTeX

$$$ \text{Sum.elim } (\Pi.mulSingle i c) (1 : β \to γ) = \Pi.mulSingle (\text{Sum.inl } i) c $$$

Lean4

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

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