prodCongrLeft — Mathlib

English

A family of equivalences a ↦ e(a) yields an equivalence between β₁ × α₁ and β₂ × α₁.

Русский

Семейство эквивалентностей a ↦ e(a) порождает эквивалентность β₁ × α₁ ≃ β₂ × α₁.

LaTeX

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

Lean4

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

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