feat: add missing lemma Fintype.bddBelow_range (#4739)

leanprover-community · Jun 7, 2023 · 3b23c3a · 3b23c3a
1 parent ea80818
commit 3b23c3a
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/Mathlib/Data/Fintype/Order.lean b/Mathlib/Data/Fintype/Order.lean
@@ -204,10 +204,21 @@ theorem Fintype.exists_le [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)
   directed_id.fintype_le _
 #align fintype.exists_le Fintype.exists_le
 
+theorem Fintype.exists_ge [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {β : Type _} [Fintype β]
+    (f : β → α) : ∃ M, ∀ i, M ≤ f i :=
+  directed_id.fintype_le (r := (· ≥ ·)) _
+
 theorem Fintype.bddAbove_range [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {β : Type _}
     [Fintype β] (f : β → α) : BddAbove (Set.range f) := by
   obtain ⟨M, hM⟩ := Fintype.exists_le f
   refine' ⟨M, fun a ha => _⟩
   obtain ⟨b, rfl⟩ := ha
   exact hM b
 #align fintype.bdd_above_range Fintype.bddAbove_range
+
+theorem Fintype.bddBelow_range [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] {β : Type _}
+    [Fintype β] (f : β → α) : BddBelow (Set.range f) := by
+  obtain ⟨M, hM⟩ := Fintype.exists_ge f
+  refine' ⟨M, fun a ha => _⟩
+  obtain ⟨b, rfl⟩ := ha
+  exact hM b