orderBornology

Mathlib.Topology.Order.Bornology

URI: https://scilib.ai/kg/mathlib#orderBornology

Lean4

/-- Order-bornology on a nonempty lattice. The bounded sets are the sets that are bounded both above
and below. -/
def orderBornology : Bornology α :=
  .ofBounded {s | BddBelow s ∧ BddAbove s} (by simp) (fun _ hs _ hst ↦ ⟨hs.1.mono hst, hs.2.mono hst⟩)
    (fun _ hs _ ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩) (by simp)

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

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

Разделы

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

Аффилиация

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