lift

Mathlib.Order.BoundedOrder.Basic

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

Lean4

/-- Pullback a `BoundedOrder`. -/
abbrev lift [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β) (map_le : ∀ a b, f a ≤ f b → a ≤ b)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : BoundedOrder α
    where
  __ := OrderTop.lift f map_le map_top
  __ := OrderBot.lift f map_le map_bot

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

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

Разделы

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

Аффилиация

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