lift

Mathlib.Order.BoundedOrder.Basic

URI: https://scilib.ai/kg/mathlib#OrderBot.lift

Lean4

/-- Pullback an `OrderBot`. -/
abbrev lift [LE α] [Bot α] [LE β] [OrderBot β] (f : α → β) (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_bot : f ⊥ = ⊥) :
    OrderBot α :=
  ⟨fun a =>
    map_le _ _ <| by
      rw [map_bot]
      exact bot_le _⟩
    -- See note [reducible non-instances]

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

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

Разделы

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

Аффилиация

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