Theorems · Definition · logic and foundations

Equiv.prodCongrRight

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

A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence between α₁ × β₁ and α₁ × β₂.

Defined in

Mathlib.Logic.Equiv.Prod

Cited by

12 results in Mathlib

Foundations

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