sumLexCongr_symm — Mathlib

English

The symmetric of sumLexCongr equals the sumLexCongr of the symmetric: (ea.sumLexCongr eb).symm = ea.symm.sumLexCongr eb.symm.

Русский

Обратное к sumLexCongr равно sumLexCongr от обратных: (ea.sumLexCongr eb).symm = ea.symm.sumLexCongr eb.symm.

LaTeX

$$$ (ea.sumLexCongr eb).\mathrm{symm} = ea.symm.sumLexCongr eb.symm $$$

Lean4

@[simp]
theorem sumLexCongr_symm (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) : (ea.sumLexCongr eb).symm = ea.symm.sumLexCongr eb.symm :=
  rfl

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