eHomCongr_refl — Mathlib

English

The congruence map eHomCongr on identity is itself the identity morphism.

Русский

Соответствующая конгруэнтность eHomCongr на тождественный изоморфизм совпадает с тождественным морфизмом.

LaTeX

$$$\mathrm{eHomCongr}(V, \mathrm{Iso.refl}X, \mathrm{Iso.refl}Y) = \mathrm{Iso.refl}(X \to[V] Y).$$$

Lean4

theorem eHomCongr_refl (X Y : C) : eHomCongr V (Iso.refl X) (Iso.refl Y) = Iso.refl (X ⟶[V] Y) := by aesop

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