prodExtendRight — Mathlib

English

For any f : α ⊕ β → γ and b : β, (sumArrowEquivProdArrow α β γ f).2 b = f (inr b).

Русский

Для любого f : α ⊕ β → γ и b : β, (sumArrowEquivProdArrow α β γ f).snd b = f (inr b).

LaTeX

$$$(\text{sumArrowEquivProdArrow }\alpha\beta\gamma\ f).2\ b = f(\text{inr } b)$$$

Lean4

/-- `prodExtendRight a e` extends `e : Perm β` to `Perm (α × β)` by sending `(a, b)` to
`(a, e b)` and keeping the other `(a', b)` fixed. -/
def prodExtendRight : Perm (α₁ × β₁)
    where
  toFun ab := if ab.fst = a then (a, e ab.snd) else ab
  invFun ab := if ab.fst = a then (a, e.symm ab.snd) else ab
  left_inv := by grind
  right_inv := by grind

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