arrowCongr_refl — Mathlib

English

The map arrowCongr with reflexivities is the reflexive arrowCongr on function spaces: arrowCongr (refl α) (refl β) = refl (α → β).

Русский

Стрелочный конгрур с тождествами даёт тождественную стрелку: arrowCongr (refl α) (refl β) = refl (α → β).

LaTeX

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

Lean4

@[simp]
theorem arrowCongr_refl {α β : Sort*} : arrowCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β) :=
  rfl

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