const_comp

Mathlib.Topology.Category.CompHausLike.Basic

URI: https://scilib.ai/kg/mathlib#CompHausLike.const_comp

Lean4

theorem const_comp {P : TopCat.{u} → Prop} {S T U : CompHausLike.{u} P} (s : S) (g : S ⟶ U) :
    T.const s ≫ g = T.const (g s) :=
  rfl

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

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

Разделы

Аффилиация

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