map

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ContinuousHom.map

Lean4

/-- `Part.map` as a continuous function. -/
@[simps! apply]
noncomputable def map {β γ : Type v} (f : β → γ) (g : α →𝒄 Part β) : α →𝒄 Part γ :=
  .copy (fun x => f <$> g x) (bind g (const (pure ∘ f))) <|
    by
    ext1
    simp only [map_eq_bind_pure_comp, bind, coe_mk, OrderHom.partBind_coe, coe_apply, coe_toOrderHom, const_apply,
      Part.bind_eq_bind]

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

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

Разделы

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

Аффилиация

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