arrowCongr'_trans — Mathlib

English

Refl and transitivity for arrowCongr' hold: arrowCongr' (refl α) (refl β) = refl (α → β) and arrowCongr'_trans (e1) (e1') (e2) (e2') similar to the Type version.

Русский

Рефлексивность и транзитивность для arrowCongr' сохраняются.

LaTeX

$$$\text{arrowCongr' }(\mathrm{refl}\, \alpha)(\mathrm{refl}\, \beta) = \mathrm{refl}\,(\alpha \to \beta)$$$

Lean4

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

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