sumPSum — Mathlib

English

Combine two equivalences by using Sum in the domain and PSum in the codomain; obtain an equivalence between Sum α1 β1 and PSum α2 β2.

Русский

Используя Sum в области и PSum в кодомене, получаем эквив между Sum α1 β1 и PSum α2 β2.

LaTeX

$$def sumPSum (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : Sum α₁ β₁ ≃ PSum α₂ β₂$$

Lean4

/-- Combine two `Equiv`s using `Sum` in the domain and `PSum` in the codomain. -/
def sumPSum {α₁ β₁} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕' β₂ :=
  (ea.symm.psumSum eb.symm).symm

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