arrowCongr'_refl — Mathlib

English

The Type version is preserved under 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'_refl {α β : Type*} : arrowCongr' (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β) :=
  rfl

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