orderBot

Mathlib.Order.BoundedOrder.Basic

URI: https://scilib.ai/kg/mathlib#Subtype.orderBot

Lean4

/-- A subtype remains a `⊥`-order if the property holds at `⊥`. -/
protected abbrev orderBot [LE α] [OrderBot α] (hbot : p ⊥) : OrderBot { x : α // p x }
    where
  bot := ⟨⊥, hbot⟩
  bot_le _ := bot_le

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

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

Разделы

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

Аффилиация

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