Mathlib.Topology.Order.Bornology

orderBornology definition

: Bornology α

Full source

/-- 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)

Order-bornology on a lattice

Informal description

The order-bornology on a nonempty lattice $\alpha$ is defined as the bornology where the bounded sets are exactly those that are both bounded below and bounded above. In other words, a set $s \subseteq \alpha$ is bounded in this bornology if and only if there exist elements $a, b \in \alpha$ such that $a \leq x \leq b$ for all $x \in s$.

orderBornology_isBounded theorem

: orderBornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

Full source

@[simp] lemma orderBornology_isBounded : orderBornologyorderBornology.IsBounded s ↔ BddBelow s ∧ BddAbove s := by
  simp [IsBounded, IsCobounded, -isCobounded_compl_iff]

Characterization of Order-Bornology Bounded Sets: $\text{IsBounded}(s) \leftrightarrow \text{BddBelow}(s) \land \text{BddAbove}(s)$

Informal description

A set $s$ in a nonempty lattice $\alpha$ is bounded in the order-bornology if and only if $s$ is both bounded below and bounded above. That is, $s$ is order-bornology-bounded precisely when there exist elements $a, b \in \alpha$ such that $a \leq x \leq b$ for all $x \in s$.

IsOrderBornology structure

Full source

/-- 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. -/
class IsOrderBornology : Prop where
  protected isBounded_iff_bddBelow_bddAbove (s : Set α) : IsBoundedIsBounded s ↔ BddBelow s ∧ BddAbove s

Order-Bornology Property

Informal description

A preorder is said to have the order-bornology property if its bounded sets are precisely those that are both bounded above and bounded below. In other words, a set is bounded in this bornology if and only if it has both lower and upper bounds.

isOrderBornology_iff_eq_orderBornology theorem

[Lattice α] [Nonempty α] : IsOrderBornology α ↔ ‹Bornology α› = orderBornology

Full source

lemma isOrderBornology_iff_eq_orderBornology [Lattice α] [Nonempty α] :
    IsOrderBornologyIsOrderBornology α ↔ ‹Bornology α› = orderBornology := by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩
  ext s
  exact isBounded_compl_iff.symm.trans (h.1 _)

Characterization of Order-Bornology: $\text{IsOrderBornology}(\alpha) \leftrightarrow \text{Bornology}(\alpha) = \text{orderBornology}$

Informal description

For a nonempty lattice $\alpha$, the bornology on $\alpha$ has the order-bornology property if and only if it coincides with the order-bornology (where bounded sets are exactly those that are both bounded below and bounded above). That is, $\text{IsOrderBornology}(\alpha) \leftrightarrow \text{Bornology}(\alpha) = \text{orderBornology}$.

isBounded_iff_bddBelow_bddAbove theorem

: IsBounded s ↔ BddBelow s ∧ BddAbove s

Full source

lemma isBounded_iff_bddBelow_bddAbove : IsBoundedIsBounded s ↔ BddBelow s ∧ BddAbove s :=
  IsOrderBornology.isBounded_iff_bddBelow_bddAbove _

Characterization of Bounded Sets in Order-Bornology: $s$ is bounded $\iff$ $s$ is bounded below and above

Informal description

A set $s$ in a preorder with the order-bornology property is bounded if and only if it is both bounded below and bounded above.

Bornology.IsBounded.bddBelow theorem

(hs : IsBounded s) : BddBelow s

Full source

protected lemma Bornology.IsBounded.bddBelow (hs : IsBounded s) : BddBelow s :=
  (isBounded_iff_bddBelow_bddAbove.1 hs).1

Boundedness in Order-Bornology Implies Lower Boundedness

Informal description

If a set $s$ is bounded in the order-bornology of a preorder, then $s$ is bounded below.

Bornology.IsBounded.bddAbove theorem

(hs : IsBounded s) : BddAbove s

Full source

protected lemma Bornology.IsBounded.bddAbove (hs : IsBounded s) : BddAbove s :=
  (isBounded_iff_bddBelow_bddAbove.1 hs).2

Boundedness in Order-Bornology Implies Upper Boundedness

Informal description

If a set $s$ is bounded in the order-bornology of a preorder, then $s$ is bounded above.

BddBelow.isBounded theorem

(hs₀ : BddBelow s) (hs₁ : BddAbove s) : IsBounded s

Full source

protected lemma BddBelow.isBounded (hs₀ : BddBelow s) (hs₁ : BddAbove s) : IsBounded s :=
  isBounded_iff_bddBelow_bddAbove.2 ⟨hs₀, hs₁⟩

Boundedness from Lower and Upper Bounds in Order-Bornology

Informal description

For any set $s$ in a preorder with the order-bornology property, if $s$ is both bounded below and bounded above, then $s$ is bounded in the order-bornology.

BddAbove.isBounded theorem

(hs₀ : BddAbove s) (hs₁ : BddBelow s) : IsBounded s

Full source

protected lemma BddAbove.isBounded (hs₀ : BddAbove s) (hs₁ : BddBelow s) : IsBounded s :=
  isBounded_iff_bddBelow_bddAbove.2 ⟨hs₁, hs₀⟩

Boundedness from Upper and Lower Bounds in Order-Bornology

Informal description

For any set $s$ in a preorder with the order-bornology property, if $s$ is both bounded above and bounded below, then $s$ is bounded in the order-bornology.

BddBelow.isBounded_inter theorem

(hs : BddBelow s) (ht : BddAbove t) : IsBounded (s ∩ t)

Full source

lemma BddBelow.isBounded_inter (hs : BddBelow s) (ht : BddAbove t) : IsBounded (s ∩ t) :=
  (hs.mono inter_subset_left).isBounded <| ht.mono inter_subset_right

Boundedness of Intersection under Lower and Upper Bounds in Order-Bornology

Informal description

For any sets $s$ and $t$ in a preorder with the order-bornology property, if $s$ is bounded below and $t$ is bounded above, then their intersection $s \cap t$ is bounded in the order-bornology.

BddAbove.isBounded_inter theorem

(hs : BddAbove s) (ht : BddBelow t) : IsBounded (s ∩ t)

Full source

lemma BddAbove.isBounded_inter (hs : BddAbove s) (ht : BddBelow t) : IsBounded (s ∩ t) :=
  (hs.mono inter_subset_left).isBounded <| ht.mono inter_subset_right

Boundedness of Intersection under Upper and Lower Bounds in Order-Bornology

Informal description

For any sets $s$ and $t$ in a preorder with the order-bornology property, if $s$ is bounded above and $t$ is bounded below, then their intersection $s \cap t$ is bounded in the order-bornology.

OrderDual.instIsOrderBornology instance

: IsOrderBornology αᵒᵈ

Full source

instance OrderDual.instIsOrderBornology : IsOrderBornology αᵒᵈ where
  isBounded_iff_bddBelow_bddAbove s := by
    rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]

Order-Bornology Structure on Order Dual

Informal description

The order dual $\alpha^\mathrm{op}$ of a preorder $\alpha$ with order-bornology is also equipped with the order-bornology structure.

Prod.instIsOrderBornology instance

{β : Type*} [Preorder β] [Bornology β] [IsOrderBornology β] : IsOrderBornology (α × β)

Full source

instance Prod.instIsOrderBornology {β : Type*} [Preorder β] [Bornology β] [IsOrderBornology β] :
    IsOrderBornology (α × β) where
  isBounded_iff_bddBelow_bddAbove s := by
    rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]

Order-Bornology Structure on Product Preorders

Informal description

For any two preorders $\alpha$ and $\beta$ each equipped with their order-bornology structure, the product preorder $\alpha \times \beta$ is also equipped with the order-bornology structure, where a set is bounded if and only if it is bounded in both components.

Pi.instIsOrderBornology instance

 {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, Bornology (α i)] [∀ i, IsOrderBornology (α i)] :
  IsOrderBornology (∀ i, α i)

Full source

instance Pi.instIsOrderBornology {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)]
    [∀ i, Bornology (α i)] [∀ i, IsOrderBornology (α i)] : IsOrderBornology (∀ i, α i) where
  isBounded_iff_bddBelow_bddAbove s := by
    simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]

Order-Bornology Structure on Product of Preorders

Informal description

For any family of preorders $\{\alpha_i\}_{i \in \iota}$ each equipped with their order-bornology (where bounded sets are precisely those that are both bounded above and below), the product preorder $\prod_{i} \alpha_i$ is also equipped with the order-bornology structure.

Bornology.IsBounded.subset_Icc_sInf_sSup theorem

(hs : IsBounded s) : s ⊆ Icc (sInf s) (sSup s)

Full source

protected lemma Bornology.IsBounded.subset_Icc_sInf_sSup (hs : IsBounded s) :
    s ⊆ Icc (sInf s) (sSup s) := subset_Icc_csInf_csSup hs.bddBelow hs.bddAbove

Bounded Sets are Contained in Their Infimum-Supremum Interval

Informal description

For any set $s$ in a conditionally complete lattice equipped with the order-bornology, if $s$ is bounded in this bornology, then $s$ is contained in the closed interval between its infimum and supremum, i.e., $s \subseteq [\inf s, \sup s]$.

Main declarations