prodCongrRight — Mathlib

English

For e : α₁ → β₁ ≃ β₂, there is an equivalence α₁ × β₁ ≃ α₁ × β₂ sending (a,b) to (a, e a b).

Русский

Для e : α₁ → β₁ ≃ β₂ существует эквивалентность α₁ × β₁ ≃ α₁ × β₂, переводящая (a,b) в (a, e a b).

LaTeX

$$$\alpha_1 \times \beta_1 \cong \alpha_1 \times \beta_2$, $(a,b) \mapsto (a, e(a)(b))$$$

Lean4

/-- A family of equivalences `∀ (a : α₁), β₁ ≃ β₂` generates an equivalence
between `α₁ × β₁` and `α₁ × β₂`. -/
def prodCongrRight : α₁ × β₁ ≃ α₁ × β₂ where
  toFun ab := ⟨ab.1, e ab.1 ab.2⟩
  invFun ab := ⟨ab.1, (e ab.1).symm ab.2⟩
  left_inv := by grind
  right_inv := by grind

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