arrowCongr_trans — Mathlib

English

A version of arrowCongr with transitivity: arrowCongr (e1.trans e2) (e1'.trans e2') = (arrowCongr e1 e1').trans (arrowCongr e2 e2').

Русский

Версия arrowCongr с транспозицией: arrowCongr (e1.trans e2) (e1'.trans e2') = (arrowCongr e1 e1').trans (arrowCongr e2 e2').

LaTeX

$$$\text{arrowCongr }(e1.\trans e2) (e1'.\trans e2') = (\text{arrowCongr } e1 e1').trans (\text{arrowCongr } e2 e2')$$$

Lean4

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

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