feat(Order/ConditionallyCompleteLattice/Basic): not_mem_of_lt_csInf' (

#16988)
leanprover-community · Sep 21, 2024 · ddb07e5 · ddb07e5
1 parent 94533cc
commit ddb07e5
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
@@ -1212,6 +1212,9 @@ theorem exists_lt_of_lt_ciSup' {f : ι → α} {a : α} (h : a < ⨆ i, f i) :
   contrapose! h
   exact ciSup_le' h
 
+theorem not_mem_of_lt_csInf' {x : α} {s : Set α} (h : x < sInf s) : x ∉ s :=
+  not_mem_of_lt_csInf h (OrderBot.bddBelow s)
+
 theorem ciSup_mono' {ι'} {f : ι → α} {g : ι' → α} (hg : BddAbove (range g))
     (h : ∀ i, ∃ i', f i ≤ g i') : iSup f ≤ iSup g :=
   ciSup_le' fun i => Exists.elim (h i) (le_ciSup_of_le hg)