Theorems · Definition · logic and foundations

Equiv.prodCongr

{α₁ : Type u_9} → {α₂ : Type u_10} → {β₁ : Type u_11} → {β₂ : Type u_12} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂

Product of two equivalences. If α₁ ≃ α₂ and β₁ ≃ β₂, then α₁ × β₁ ≃ α₂ × β₂. This is Prod.map as an equivalence.

Defined in

Mathlib.Logic.Equiv.Prod

Cited by

24 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound