prodPProd — Mathlib

English

Combine two equivalences ea and eb in the opposite direction: α₁ × β₁ ≃ PProd α₂ β₂ by using the inverses of ea and eb.

Русский

Соединение двух эквивалентностей в обратном направлении: α₁ × β₁ ≃ PProd α₂ β₂ через обратные ea и eb.

LaTeX

$$$\\text{prodPProd }\\{α₁ β₁} (ea: α₁\\simeq α₂) (eb: β₁\\simeq β₂) : α₁ × β₁ \\simeq PProd α₂ β₂$$$

Lean4

/-- Combine two equivalences using `PProd` in the codomain and `Prod` in the domain. -/
@[simps! (attr := grind =) apply symm_apply]
def prodPProd {α₁ β₁} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ × β₁ ≃ PProd α₂ β₂ :=
  (ea.symm.pprodProd eb.symm).symm

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