English
Product of two equivalences, using PProd in the domain and Prod in the codomain: combine ea : α₁ ≃ α₂ and eb : β₁ ≃ β₂ into an equivalence α₁ × β₁ ≃ PProd α₂ β₂.
Русский
Произведение двух эквивалентностей с использованием PProd в области определения и Prod в области кодирования: соединить ea и eb в эквивалентность α₁ × β₁ ≃ PProd α₂ β₂.
LaTeX
$$$\\text{pprodProd }\\{α₁ β₁} \\{α₂ β₂} (ea: α₁\\simeq α₂) (eb: β₁\\simeq β₂) : α₁ × β₁ \\simeq PProd α₂ β₂$$$
Lean4
/-- `PProd α β` is equivalent to `α × β` -/
@[simps (attr := grind =) apply symm_apply]
def pprodEquivProd {α β} : PProd α β ≃ α × β where
toFun x := (x.1, x.2)
invFun x := ⟨x.1, x.2⟩
