embeddingCongr_symm — Mathlib

English

The congruence maps commute with taking inverses: (embeddingCongr e1 e2)^{-1} = e1^{-1}.embeddingCongr e2^{-1}.

Русский

Согласование вложений обращается к инверсии через соответствующие пары эквивалентностей.

LaTeX

$$$(\\text{embeddingCongr } e_1 e_2)^{\\, -1} = (e_1^{ -1})\\text{.embeddingCongr}(e_2^{ -1})$$$

Lean4

@[simp]
theorem embeddingCongr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
    (embeddingCongr e₁ e₂).symm = embeddingCongr e₁.symm e₂.symm :=
  rfl

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