Theorems · Definition · logic and foundations

Equiv.prodShear

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

A variation on Equiv.prodCongr where the equivalence in the second component can depend on the first component. A typical example is a shear mapping, explaining the name of this declaration.

Defined in

Mathlib.Logic.Equiv.Prod

Cited by

5 results in Mathlib

Foundations

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