equiv_inr — Mathlib

English

Define fromSum as the map ι1 ⊕ ι2 → ι by sending Sum.inl i1 to e1.f i1 and Sum.inr i2 to e2.f i2.

Русский

Задаётся отображение fromSum: ι1 ⊕ ι2 → ι, отправляющее Sum.inl i1 в e1.f i1 и Sum.inr i2 в e2.f i2.

LaTeX

$$$\mathrm{fromSum} : (ι_1 \oplus ι_2) \to ι,\qquad \mathrm{fromSum}(\mathrm{Sum.inl}(i_1)) = e_1.f(i_1),\; \mathrm{fromSum}(\mathrm{Sum.inr}(i_2)) = e_2.f(i_2).$$$

Lean4

@[simp]
theorem equiv_inr (i₂ : ι₂) : ac.equiv (Sum.inr i₂) = e₂.f i₂ :=
  rfl

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