base_mk

Mathlib.CategoryTheory.Bicategory.CatEnriched

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatEnrichedOrdinary.base_mk

English

The base of Hom.mk(α) equals α: base(Hom.mk(α)) = α.

Русский

База Hom.mk(α) равна α: base(Hom.mk(α)) = α.

LaTeX

$$$ base( Hom.mk(\\alpha) ) = \\alpha $$$

Lean4

@[simp]
theorem base_mk {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : homEquiv f ⟶ homEquiv g) : Hom.base (Hom.mk α) = α :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru