psumCongr — Mathlib

English

If e1 : α ≃ β and e2 : γ ≃ δ, then α ⊕' γ ≃ β ⊕' δ via PSum with e1,e2.

Русский

Если e1: α ≃ β и e2: γ ≃ δ, то α ⊕' γ ≃ β ⊕' δ через PSum.

LaTeX

$$def psumCongr (e1 : α ≃ β) (e2 : γ ≃ δ) : α ⊕' γ ≃ β ⊕' δ$$

Lean4

/-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕' β ≃ α' ⊕' β'`. -/
def psumCongr (e₁ : α ≃ β) (e₂ : γ ≃ δ) : α ⊕' γ ≃ β ⊕' δ
    where
  toFun x := PSum.casesOn x (PSum.inl ∘ e₁) (PSum.inr ∘ e₂)
  invFun x := PSum.casesOn x (PSum.inl ∘ e₁.symm) (PSum.inr ∘ e₂.symm)
  left_inv := by rintro (x | x) <;> simp
  right_inv := by rintro (x | x) <;> simp

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