arrowCongrLeft_refl — Mathlib

English

The arrowCongrLeft of the reflexive embedding is the reflexive embedding on functions: (refl α).arrowCongrLeft (γ) = refl (α → γ).

Русский

Объединение стрелок через рефлексивное вложение даёт тождественное вложение на функции: (refl α).arrowCongrLeft (γ) = refl (α → γ).

LaTeX

$$$ (\\mathrm{refl}_\\alpha).\\mathrm{arrowCongrLeft} (\\gamma := \\gamma) = \\mathrm{refl}_{\\alpha \\to \\gamma}$$$

Lean4

@[simp]
theorem arrowCongrLeft_refl {α : Sort u} {γ : Sort w} [Inhabited γ] :
    (Function.Embedding.refl α).arrowCongrLeft (γ := γ) = .refl _ :=
  by
  ext
  simp [coe_refl]

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