feat(order/bounds): add basic lemmas about bdd_below (#5186)

Lemmas for bounded intervals (`Icc`, `Ico`, `Ioc` and `Ioo`). There were lemmas for `bdd_above` but the ones for `bdd_below` were missing.
leanprover-community · Dec 2, 2020 · 9be829e · 9be829e
1 parent e5befed
commit 9be829e
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/order/bounds.lean b/src/order/bounds.lean
@@ -354,12 +354,20 @@ lemma bdd_below_singleton : bdd_below ({a} : set α) := is_glb_singleton.bdd_bel
 
 lemma bdd_above_Icc : bdd_above (Icc a b) := ⟨b, λ _, and.right⟩
 
+lemma bdd_below_Icc : bdd_below (Icc a b) := ⟨a, λ _, and.left⟩
+
 lemma bdd_above_Ico : bdd_above (Ico a b) := bdd_above_Icc.mono Ico_subset_Icc_self
 
+lemma bdd_below_Ico : bdd_below (Ico a b) := bdd_below_Icc.mono Ico_subset_Icc_self
+
 lemma bdd_above_Ioc : bdd_above (Ioc a b) := bdd_above_Icc.mono Ioc_subset_Icc_self
 
+lemma bdd_below_Ioc : bdd_below (Ioc a b) := bdd_below_Icc.mono Ioc_subset_Icc_self
+
 lemma bdd_above_Ioo : bdd_above (Ioo a b) := bdd_above_Icc.mono Ioo_subset_Icc_self
 
+lemma bdd_below_Ioo : bdd_below (Ioo a b) := bdd_below_Icc.mono Ioo_subset_Icc_self
+
 lemma is_greatest_Icc (h : a ≤ b) : is_greatest (Icc a b) b :=
 ⟨right_mem_Icc.2 h, λ x, and.right⟩