Documentation

Mathlib.Topology.Order.Bornology

Bornology of order-bounded sets #

This file relates the notion of bornology-boundedness (sets that lie in a bornology) to the notion of order-boundedness (sets that are bounded above and below).

Main declarations #

def orderBornology {α : Type u_1} [Lattice α] [Nonempty α] :

Order-bornology on a nonempty lattice. The bounded sets are the sets that are bounded both above and below.

Equations
Instances For
    @[simp]
    class IsOrderBornology (α : Type u_1) [Bornology α] [Preorder α] :

    Predicate for a preorder to be equipped with its order-bornology, namely for its bounded sets to be the ones that are bounded both above and below.

    Instances
      theorem isOrderBornology_iff_eq_orderBornology {α : Type u_1} [Bornology α] [Lattice α] [Nonempty α] :
      IsOrderBornology α inst✝² = orderBornology
      theorem BddBelow.isBounded {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs₀ : BddBelow s) (hs₁ : BddAbove s) :
      theorem BddAbove.isBounded {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs₀ : BddAbove s) (hs₁ : BddBelow s) :
      theorem BddBelow.isBounded_inter {α : Type u_1} {s : Set α} {t : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs : BddBelow s) (ht : BddAbove t) :
      theorem BddAbove.isBounded_inter {α : Type u_1} {s : Set α} {t : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs : BddAbove s) (ht : BddBelow t) :
      instance Prod.instIsOrderBornology {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] {β : Type u_2} [Preorder β] [Bornology β] [IsOrderBornology β] :
      Equations
      • =
      instance Pi.instIsOrderBornology {ι : Type u_2} {α : ιType u_3} [(i : ι) → Preorder (α i)] [(i : ι) → Bornology (α i)] [∀ (i : ι), IsOrderBornology (α i)] :
      IsOrderBornology ((i : ι) → α i)
      Equations
      • =