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

• orderBornology: The bornology of order-bounded sets of a nonempty lattice.
• IsOrderBornology: Typeclass predicate for a preorder to be equipped with its order-bornology.

@[instance_reducible]

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

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

Equations

• orderBornology = Bornology.ofBounded {s : Set α | BddBelow s ∧ BddAbove s} ⋯ ⋯ ⋯ ⋯

@[simp]

theorem orderBornology_isBounded {α : Type u_1} {s : Set α} [Lattice α] [Nonempty α] : Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

class IsOrderBornology (α : Type u_1) [Bornology α] [Preorder α] : Prop

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.

• isBounded_iff_bddBelow_bddAbove (s : Set α) : Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

theorem isOrderBornology_iff_eq_orderBornology {α : Type u_1} [Bornology α] [Lattice α] [Nonempty α] : IsOrderBornology α ↔ inst✝ = orderBornology

theorem isBounded_iff_bddBelow_bddAbove {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] : Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

theorem Bornology.IsBounded.bddBelow {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs : IsBounded s) : BddBelow s

theorem Bornology.IsBounded.bddAbove {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs : IsBounded s) : BddAbove s

theorem BddBelow.isBounded {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs₀ : BddBelow s) (hs₁ : BddAbove s) : Bornology.IsBounded s

theorem BddAbove.isBounded {α : Type u_1} {s : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs₀ : BddAbove s) (hs₁ : BddBelow s) : Bornology.IsBounded s

theorem BddBelow.isBounded_inter {α : Type u_1} {s t : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs : BddBelow s) (ht : BddAbove t) : Bornology.IsBounded (s ∩ t)

theorem BddAbove.isBounded_inter {α : Type u_1} {s t : Set α} [Bornology α] [Preorder α] [IsOrderBornology α] (hs : BddAbove s) (ht : BddBelow t) : Bornology.IsBounded (s ∩ t)

instance OrderDual.instIsOrderBornology {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] : IsOrderBornology αᵒᵈ

instance Prod.instIsOrderBornology {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] {β : Type u_2} [Preorder β] [Bornology β] [IsOrderBornology β] : IsOrderBornology (α × β)

instance Pi.instIsOrderBornology {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Preorder (α i)] [(i : ι) → Bornology (α i)] [∀ (i : ι), IsOrderBornology (α i)] : IsOrderBornology ((i : ι) → α i)

theorem Nonempty.of_isOrderBornology (α : Type u_1) [Bornology α] [Preorder α] [IsOrderBornology α] : Nonempty α

instance IsOrderBornology.neBot_cobounded_of_noBotOrder {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] [NoBotOrder α] : (Bornology.cobounded α).NeBot

instance IsOrderBornology.neBot_cobounded_of_noTopOrder {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] [NoTopOrder α] : (Bornology.cobounded α).NeBot

theorem IsOrderBornology.atTop_le_cobounded {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] [NoMaxOrder α] : Filter.atTop ≤ Bornology.cobounded α

theorem IsOrderBornology.atBot_le_cobounded {α : Type u_1} [Bornology α] [Preorder α] [IsOrderBornology α] [NoMinOrder α] : Filter.atBot ≤ Bornology.cobounded α

theorem IsOrderBornology.cobounded_le_atBot_sup_atTop {α : Type u_1} [Bornology α] [LinearOrder α] [IsOrderBornology α] : Bornology.cobounded α ≤ Filter.atBot ⊔ Filter.atTop

@[simp]

theorem IsOrderBornology.cobounded_eq {α : Type u_1} [Bornology α] [LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [NoMinOrder α] : Bornology.cobounded α = Filter.atBot ⊔ Filter.atTop

theorem IsOrderBornology.cobounded_eq_atTop {α : Type u_1} [Bornology α] [LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [OrderBot α] : Bornology.cobounded α = Filter.atTop

theorem IsOrderBornology.cobounded_eq_atBot {α : Type u_1} [Bornology α] [LinearOrder α] [IsOrderBornology α] [NoMinOrder α] [OrderTop α] : Bornology.cobounded α = Filter.atBot

theorem Bornology.IsBounded.subset_Icc_sInf_sSup {α : Type u_1} [Bornology α] [ConditionallyCompleteLattice α] [IsOrderBornology α] {s : Set α} (hs : IsBounded s) : s ⊆ Set.Icc (sInf s) (sSup s)