sumCongr_symm — Mathlib

English

Let ea: α1 ≃o α2 and eb: β1 ≃o β2 be order isomorphisms. Then the symmetry of the sum-congruence equals the sum-congruence of the symmetries: (ea.sumCongr eb).symm = ea.symm.sumCongr eb.symm.

Русский

Пусть ea: α1 ≃o α2 и eb: β1 ≃o β2 — порядковые изоморфизмы. Тогда симметрия сумм-конгруэнтности равна сумме симметрий: (ea.sumCongr eb).symm = ea.symm.sumCongr eb.symm.

LaTeX

$$$ (ea.sumCongr eb).\mathrm{symm} = ea^{-1}.sumCongr eb^{-1} $$$

Lean4

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

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