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.
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.isBounded_iff_bddBelow_bddAbove
{α : Type u_1}
:
∀ {inst : Bornology α} {inst_1 : Preorder α} [self : IsOrderBornology α] (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 : Bornology.IsBounded s)
:
BddBelow s
theorem
Bornology.IsBounded.bddAbove
{α : Type u_1}
{s : Set α}
[Bornology α]
[Preorder α]
[IsOrderBornology α]
(hs : Bornology.IsBounded s)
:
BddAbove s
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)
:
Bornology.IsBounded (s ∩ t)
theorem
BddAbove.isBounded_inter
{α : Type u_1}
{s : Set α}
{t : Set α}
[Bornology α]
[Preorder α]
[IsOrderBornology α]
(hs : BddAbove s)
(ht : BddBelow t)
:
Bornology.IsBounded (s ∩ t)
instance
OrderDual.instIsOrderBornology
{α : Type u_1}
[Bornology α]
[Preorder α]
[IsOrderBornology α]
:
Equations
- ⋯ = ⋯
instance
Prod.instIsOrderBornology
{α : Type u_1}
[Bornology α]
[Preorder α]
[IsOrderBornology α]
{β : Type u_2}
[Preorder β]
[Bornology β]
[IsOrderBornology β]
:
IsOrderBornology (α × β)
Equations
- ⋯ = ⋯
instance
Pi.instIsOrderBornology
{ι : Type u_2}
{α : ι → Type u_3}
[(i : ι) → Preorder (α i)]
[(i : ι) → Bornology (α i)]
[∀ (i : ι), IsOrderBornology (α i)]
:
IsOrderBornology ((i : ι) → α i)
Equations
- ⋯ = ⋯
theorem
Bornology.IsBounded.subset_Icc_sInf_sSup
{α : Type u_1}
[Bornology α]
[ConditionallyCompleteLattice α]
[IsOrderBornology α]
{s : Set α}
(hs : Bornology.IsBounded s)
: