withBotMap

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#OneHom.withBotMap

Lean4

/-- A version of `WithBot.map` for `OneHom`s. -/
@[to_additive (attr := simps -fullyApplied) /-- A version of `WithBot.map` for `ZeroHom`s -/
    ]
protected def _root_.OneHom.withBotMap {M N : Type*} [One M] [One N] (f : OneHom M N) : OneHom (WithBot M) (WithBot N)
    where
  toFun := WithBot.map f
  map_one' := by rw [WithBot.map_one, map_one, coe_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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