embeddingCongr_trans — Mathlib

English

The congruence respects composition: composing equivalences on both sides commutes with embeddingCongr.

Русский

Согласование сохраняет композицию: компоновка эквивалентностей слева и справа совместима с вложениями.

LaTeX

$$$\\text{embeddingCongr}(e_1\\,\\mathrm{trans}\\, e_2)(e_1'\\,\\mathrm{trans}\\, e_2') = (\\text{embeddingCongr }e_1 e_1')\\mathrm{trans}(\\text{embeddingCongr }e_2 e_2')$$$

Lean4

@[simp]
theorem embeddingCongr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
    embeddingCongr (e₁.trans e₂) (e₁'.trans e₂') = (embeddingCongr e₁ e₁').trans (embeddingCongr e₂ e₂') :=
  rfl

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