prodSumDistrib_symm_apply_right — Mathlib

English

Let a = (a1, a3) ∈ α × γ. The inverse of the distributive equivalence sends inr a to (a1, inr a3).

Русский

Пусть a = (a1, a3) ∈ α × γ. Обратное отображение отправляет inr a на (a1, inr a3).

LaTeX

$$$\\\\big(\\\\mathrm{prodSumDistrib}\\\\ \\alpha\\\\ \\beta\\\\ \\gamma\\\\)^{-1}(\\\\mathrm{inr}(a)) = (a_1, \\\\mathrm{inr}(a_2)).$$$

Lean4

@[simp]
theorem prodSumDistrib_symm_apply_right {α β γ} (a : α × γ) : (prodSumDistrib α β γ).symm (inr a) = (a.1, inr a.2) :=
  rfl

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