English
Take two equivalences e₁ : α ≃ α' and e₂ : γ ≃ γ', and form an equivalence between PProd α γ and PProd α' γ' by applying e₁ to the first component and e₂ to the second.
Русский
Возьмем две эквивалентности e₁ и e₂ и получим эквивалентность между PProd α γ и PProd α' γ', применяя e₁ к первой компоненте и e₂ ко второй.
LaTeX
$$$\\text{pprodCongr}(e_1,e_2) : PProd α γ \\simeq PProd α' γ'$$$
Lean4
/-- Combine two equivalences using `PProd` in the domain and `Prod` in the codomain. -/
@[simps! (attr := grind =) apply symm_apply]
def pprodProd {α₂ β₂} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : PProd α₁ β₁ ≃ α₂ × β₂ :=
(ea.pprodCongr eb).trans pprodEquivProd
