map

Mathlib.CategoryTheory.ConcreteCategory.Bundled

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bundled.map

Lean4

/-- Map over the bundled structure -/
abbrev map (f : ∀ {α}, c α → d α) (b : Bundled c) : Bundled d :=
  ⟨b, f b.str⟩

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

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

Разделы

Аффилиация

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