mk'_homEquiv — Mathlib

English

For adjoint structures, the homEquiv of mk' equals the given homEquiv, i.e., (mk' adj).homEquiv = adj.homEquiv.

Русский

Для конструкции mk' от соответствующих структур гом-эквивалентность совпадает с заданной: (mk' adj).homEquiv = adj.homEquiv.

LaTeX

$$$ (mk' adj).homEquiv = adj.homEquiv $$$

Lean4

theorem mk'_homEquiv (adj : CoreHomEquivUnitCounit F G) : (mk' adj).homEquiv = adj.homEquiv :=
  by
  ext
  rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]

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