feat: Add finite iff bounded lemmas (#5567)

This PR adds a lemma stating that finiteness is equivalent to boundedness above and below in a locally finite lattice, 
as well as one-way versions for both types of semilattice.

Author: apnelson1

Mathlib/Order/LocallyFinite.lean

@@ -1364,4 +1364,27 @@ theorem map_subtype_embedding_Iio : (Iio a).map (Embedding.subtype p) = (Iio a :
 
 end LocallyFiniteOrderBot
 
+section Finite
+
+variable {α : Type _} {s : Set α}
+
+theorem finite_iff_bddAbove [SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α]:
+    s.Finite ↔ BddAbove s :=
+  ⟨fun h ↦ ⟨h.toFinset.sup id, fun x hx ↦ Finset.le_sup (f := id) (by simpa)⟩,
+    fun ⟨m, hm⟩ ↦ (Set.finite_Icc ⊥ m).subset (fun x hx ↦ ⟨bot_le, hm hx⟩)⟩
+
+theorem finite_iff_bddBelow [SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α] :
+    s.Finite ↔ BddBelow s :=
+  finite_iff_bddAbove (α := αᵒᵈ)
+
+theorem finite_iff_bddBelow_bddAbove [Nonempty α] [Lattice α] [LocallyFiniteOrder α] :
+    s.Finite ↔ BddBelow s ∧ BddAbove s := by
+  obtain (rfl | hs) := s.eq_empty_or_nonempty
+  · simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]
+  exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' (by simpa) id, fun x hx ↦ Finset.inf'_le id (by simpa)⟩,
+    ⟨h.toFinset.sup' (by simpa) id, fun x hx ↦ Finset.le_sup' id (by simpa)⟩⟩,
+    fun ⟨⟨a,ha⟩,⟨b,hb⟩⟩ ↦ (Set.finite_Icc a b).subset (fun x hx ↦ ⟨ha hx,hb hx⟩ )⟩
+
+end Finite
+
 end Finset