Combining BddBelow and BddAbove

Stream: Is there code for X?

[Terence Tao]

Is it worth bundling together the BddBelow and BddAbove properties into a single predicate, say OrdBounded? This would be particularly useful on the reals since in that case it is equivalent to Bornology.IsBounded. One could bundle a large number of the existing lemmas concerning BddBelow and BddAbove separately into lemmas for OrdBounded, e.g.,

import Mathlib

variable {α : Type*} [Preorder α]

def OrdBounded (s : Set α) := (BddBelow s) ∧ (BddAbove s)

lemma OrdBounded.mono ⦃s : Set α⦄ ⦃t : Set α⦄ (h : s ⊆ t) :
OrdBounded t → OrdBounded s := by
  intro hb
  exact ⟨ BddBelow.mono h hb.1, BddAbove.mono h hb.2 ⟩

@[simp]
lemma OrdBounded.icc (a b:α) : OrdBounded (Set.Icc a b) := ⟨ bddBelow_Icc, bddAbove_Icc ⟩

@[simp]
lemma OrdBounded.ico (a b:α) : OrdBounded (Set.Ico a b) := ⟨ bddBelow_Ico, bddAbove_Ico ⟩

@[simp]
lemma OrdBounded.ioc (a b:α) : OrdBounded (Set.Ioc a b) := ⟨ bddBelow_Ioc, bddAbove_Ioc ⟩

@[simp]
lemma OrdBounded.ioo (a b:α) : OrdBounded (Set.Ioo a b) := ⟨ bddBelow_Ioo, bddAbove_Ioo ⟩

lemma ordBounded_of_subset_of_icc {α : Type*} [Preorder α] {s : Set α} {a b:α} (h: s ⊆ Set.Icc a b) : OrdBounded s := OrdBounded.mono h (OrdBounded.icc a b)

lemma ordBounded_def {α : Type*} [Preorder α] {s : Set α} : OrdBounded s ↔ (∃ a b, s ⊆ Set.Icc a b) := bddBelow_bddAbove_iff_subset_Icc

lemma ordBounded_iff_bounded {s: Set ℝ} : OrdBounded s ↔  Bornology.IsBounded s := Real.isBounded_iff_bddBelow_bddAbove.symm

lemma Int.finite_iff_bounded {I: Set ℤ} : OrdBounded I ↔ Set.Finite I :=  Set.finite_iff_bddBelow_bddAbove.symm

[Anatole Dedecker]

I think what we should have is a class OrderBornology asserting that the ambient bornology on a type is the one induced by the order. But yes, we should make some API for this kind of things

[Anatole Dedecker]

In fact, I think I would also like to remove the MetricSpace -> Bornology instance (maybe localize it ?), and have a MetricBornology class, but this is an other discussion

[Terence Tao]

Anatole Dedecker said:

I think what we should have is a class OrderBornology asserting that the ambient bornology on a type is the one induced by the order. But yes, we should make some API for this kind of things

Perhaps one should have both, since `OrdBounded' only defines a bornology assuming one has meets and joins.

[Jireh Loreaux]

Anatole, having a MetricBornology class wouldn't really solve our bornology problems, would it? I thought the issue was more that we don't want it to be a class at all.

[Jireh Loreaux]

Feel free to split the discussion topic.