sumCongr — Mathlib

English

If α1 ≃ α2 and β1 ≃ β2, then α1 ⊕' β1 ≃ α2 ⊕' β2.

Русский

Если α1 ≃ α2 и β1 ≃ β2, то α1 ⊕' β1 ≃ α2 ⊕' β2.

LaTeX

$$Equiv (α1 ⊕' β1) (α2 ⊕' β2)$$

Lean4

/-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕ β ≃ α' ⊕ β'`. This is `Sum.map` as an equivalence. -/
@[simps apply]
def sumCongr {α₁ α₂ β₁ β₂} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ :=
  ⟨Sum.map ea eb, Sum.map ea.symm eb.symm, fun x => by simp, fun x => by simp⟩

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