English
A variation on Equiv.prodCongr where the second component's equivalence can depend on the first component. This yields an equivalence between α₁ × β₁ and α₂ × β₂ using a pair (e₁, e₂) with e₁ : α₁ ≃ α₂ and e₂ : α₁ → β₁ ≃ β₂.
Русский
Изменение варианта Equiv.prodCongr: второе компонентное эквивалентное отображение зависит от первого компонента; получается эквиваленция между α₁ × β₁ и α₂ × β₂ через пары (e₁, e₂).
LaTeX
$$$prodShear (e_1 : \alpha_1 \simeq \alpha_2) (e_2 : \alpha_1 \to (\beta_1 \simeq \beta_2)) : (\alpha_1 \times \beta_1) \simeq (\alpha_2 \times \beta_2)$ with toFun := fun x => (e_1 x.1, e_2 x.1 x.2), invFun := fun y => (e_1^{-1} y.1, (e_2 (e_1^{-1} y.1)).symm y.2)$$
Lean4
/-- 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. -/
@[simps -fullyApplied]
def prodShear (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂
where
toFun := fun x : α₁ × β₁ => (e₁ x.1, e₂ x.1 x.2)
invFun := fun y : α₂ × β₂ => (e₁.symm y.1, (e₂ <| e₁.symm y.1).symm y.2)
left_inv := by grind
right_inv := by grind
