diff --git a/Mathlib.lean b/Mathlib.lean
index bf25493c66cde3..ce88cfd79e2c49 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5806,6 +5806,7 @@ public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
+public import Mathlib.Order.CountableSupClosed
 public import Mathlib.Order.Cover
 public import Mathlib.Order.Defs.LinearOrder
 public import Mathlib.Order.Defs.PartialOrder
diff --git a/Mathlib/Order/CountableSupClosed.lean b/Mathlib/Order/CountableSupClosed.lean
new file mode 100644
index 00000000000000..4858441b0e8201
--- /dev/null
+++ b/Mathlib/Order/CountableSupClosed.lean
@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Data.Countable.Defs
+public import Mathlib.Order.SupClosed
+
+import Mathlib.Data.Nat.Pairing
+
+/-!
+# Sets closed under countable join/meet
+
+This file defines predicates for sets closed under countable supremum and dually for countable
+infimum.
+
+## Main declarations
+
+* `CountableSupClosed`: Predicate for a set to be closed under countable supremum.
+* `CountableInfClosed`: Predicate for a set to be closed under countable infimum.
+* `countableSupClosure`: countable Sup-closure. Smallest countable sup-closed set containing
+  a given set.
+* `countableInfClosure`: countable Inf-closure. Smallest countable inf-closed set containing
+  a given set.
+
+## Implementation notes
+
+The list of properties in this file is copied and adapted from the file about `SupClosed`.
+We should keep these files in sync.
+
+-/
+
+@[expose] public section
+
+variable {ι : Sort*} {α β : Type*} {S : Set (Set α)} {s t : Set α} {a b : α}
+
+section CompleteLattice
+
+variable [CompleteLattice α] [CompleteLattice β]
+
+section Set
+open Set
+
+/-- A set `s` is closed under countable supremum if `⨆ n, A n ∈ s` for all `A : ι → α`
+with `ι` nonempty countable and `A n ∈ s` for all `n`.
+
+The definition uses `ι = ℕ`.
+See `CountableSupClosed.iSup_mem` for a supremum over any nonempty countable type. -/
+structure CountableSupClosed (s : Set α) : Prop where
+  iSup_nat_mem : ∀ ⦃A : ℕ → α⦄ (_hA : ∀ n, A n ∈ s), ⨆ n, A n ∈ s
+
+/-- A set `s` is closed under countable infimum if `⨅ n, A n ∈ s` for all `A : ι → α`
+with `ι` nonempty countable and `A n ∈ s` for all `n`.
+
+The definition uses `ι = ℕ`.
+See `CountableInfClosed.iInf_mem` for an infimum over any nonempty countable type. -/
+@[to_dual existing]
+structure CountableInfClosed (s : Set α) : Prop where
+  iInf_nat_mem : ∀ ⦃A : ℕ → α⦄, (∀ n, A n ∈ s) → ⨅ n, A n ∈ s
+
+attribute [to_dual existing] CountableSupClosed
+
+@[to_dual]
+lemma CountableSupClosed.iSup_mem [hι : Countable ι] [Nonempty ι]
+    (hs : CountableSupClosed s) {A : ι → α} (hA : ∀ n, A n ∈ s) :
+    ⨆ n, A n ∈ s := by
+  obtain ⟨g, hg⟩ := countable_iff_exists_surjective.mp hι
+  have : ⨆ i, A i = ⨆ n, A (g n) := by rw [Function.Surjective.iSup_comp hg]
+  rw [this]
+  exact hs.iSup_nat_mem (fun n ↦ hA (g n))
+
+@[to_dual]
+lemma CountableSupClosed.sSup_mem (hs : CountableSupClosed s)
+    (A : Set α) [Countable A] [Nonempty A] (hA : ∀ a ∈ A, a ∈ s) :
+    sSup A ∈ s := by
+  rw [sSup_eq_iSup']
+  exact hs.iSup_mem fun a ↦ hA a a.2
+
+@[to_dual]
+lemma CountableSupClosed.supClosed (hs : CountableSupClosed s) : SupClosed s := by
+  intro a ha b hb
+  simpa using  hs.sSup_mem (A := {a, b}) (by grind)
+
+@[to_dual (attr := simp)] lemma countableSupClosed_singleton_bot :
+    CountableSupClosed ({⊥} : Set α) where
+  iSup_nat_mem A hA := by simpa using hA
+
+@[to_dual (attr := simp)] lemma CountableSupClosed.univ : CountableSupClosed (univ : Set α) where
+  iSup_nat_mem A hA := by simp
+
+@[to_dual]
+lemma CountableSupClosed.inter (hs : CountableSupClosed s) (ht : CountableSupClosed t) :
+    CountableSupClosed (s ∩ t) where
+  iSup_nat_mem _ hA := ⟨hs.iSup_nat_mem (fun n ↦ (hA n).1), ht.iSup_nat_mem (fun n ↦ (hA n).2)⟩
+
+@[to_dual]
+lemma CountableSupClosed.sInter (hS : ∀ s ∈ S, CountableSupClosed s) :
+    CountableSupClosed (⋂₀ S) where
+  iSup_nat_mem _ hA := fun _s hs ↦ (hS _ hs).iSup_mem fun n ↦ hA n _ hs
+
+@[to_dual]
+lemma CountableSupClosed.iInter {f : ι → Set α} (hf : ∀ i, CountableSupClosed (f i)) :
+    CountableSupClosed (⋂ i, f i) :=
+  .sInter <| forall_mem_range.2 hf
+
+lemma CountableSupClosed.directedOn (hs : CountableSupClosed s) : DirectedOn (· ≤ ·) s :=
+  hs.supClosed.directedOn
+
+@[to_dual]
+lemma CountableSupClosed.prod {t : Set β} (hs : CountableSupClosed s) (ht : CountableSupClosed t) :
+    CountableSupClosed (s ×ˢ t) where
+  iSup_nat_mem _ hA := ⟨by rw [Prod.fst_iSup]; exact hs.iSup_nat_mem (fun n ↦ (hA n).1),
+    by rw [Prod.snd_iSup]; exact ht.iSup_nat_mem (fun n ↦ (hA n).2)⟩
+
+end Set
+
+section Finset
+variable {ι : Type*} {f : ι → α} {t : Finset ι}
+
+@[to_dual]
+lemma CountableSupClosed.finsetSup'_mem (hs : CountableSupClosed s) (ht : t.Nonempty) :
+    (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s :=
+  hs.supClosed.finsetSup'_mem ht
+
+@[to_dual]
+lemma CountableSupClosed.finsetSup_mem (hs : CountableSupClosed s) (ht : t.Nonempty) :
+    (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s :=
+  Finset.sup'_eq_sup ht f ▸ hs.finsetSup'_mem ht
+
+end Finset
+
+open OrderDual
+
+@[simp] lemma countableSupClosed_preimage_toDual {s : Set αᵒᵈ} :
+    CountableSupClosed (toDual ⁻¹' s) ↔ CountableInfClosed s :=
+  ⟨fun h ↦ ⟨h.iSup_nat_mem⟩, fun h ↦ ⟨h.iInf_nat_mem⟩⟩
+
+@[simp] lemma countableInfClosed_preimage_toDual {s : Set αᵒᵈ} :
+    CountableInfClosed (toDual ⁻¹' s) ↔ CountableSupClosed s :=
+  ⟨fun h ↦ ⟨h.iInf_nat_mem⟩, fun h ↦ ⟨h.iSup_nat_mem⟩⟩
+
+@[simp] lemma countableSupClosed_preimage_ofDual {s : Set α} :
+    CountableSupClosed (ofDual ⁻¹' s) ↔ CountableInfClosed s :=
+  ⟨fun h ↦ ⟨h.iSup_nat_mem⟩, fun h ↦ ⟨h.iInf_nat_mem⟩⟩
+
+@[simp] lemma countableInfClosed_preimage_ofDual {s : Set α} :
+    CountableInfClosed (ofDual ⁻¹' s) ↔ CountableSupClosed s :=
+  ⟨fun h ↦ ⟨h.iInf_nat_mem⟩, fun h ↦ ⟨h.iSup_nat_mem⟩⟩
+
+alias ⟨_, CountableInfClosed.dual⟩ := countableSupClosed_preimage_ofDual
+alias ⟨_, CountableSupClosed.dual⟩ := countableInfClosed_preimage_ofDual
+
+/-! ## Closure -/
+
+/-- Every set generates a set closed under countable supremum. -/
+@[simps! isClosed]
+def countableSupClosure : ClosureOperator (Set α) := .ofPred
+  (fun s ↦ {a | ∃ (t : ℕ → α), (∀ n, t n ∈ s) ∧ ⨆ n, t n = a})
+  CountableSupClosed
+  (fun s a ha ↦ ⟨fun _ ↦ a, by simpa, by rw [ciSup_const]⟩)
+  (by
+    refine fun x ↦ ⟨fun A hA ↦ ?_⟩
+    choose B hB hB_eq using hA
+    refine ⟨fun n ↦ B (Nat.unpair n).1 (Nat.unpair n).2, fun _ ↦ hB _ _, ?_⟩
+    simp [iSup_unpair, ← hB_eq])
+  (by
+    rintro s₁ s₂ hs h₂ _ ⟨t, ht, rfl⟩
+    exact h₂.iSup_mem fun n ↦ hs (ht n))
+
+/-- Every set generates a set closed under countable infimum. -/
+@[to_dual existing, simps! isClosed]
+def countableInfClosure : ClosureOperator (Set α) := ClosureOperator.ofPred
+  (fun s ↦ {a | ∃ (t : ℕ → α), (∀ n, t n ∈ s) ∧ ⨅ n, t n = a})
+  CountableInfClosed
+  (fun s a ha ↦ ⟨fun _ ↦ a, by simpa, by rw [ciInf_const]⟩)
+  (by
+    refine fun x ↦ ⟨fun A hA ↦ ?_⟩
+    choose B hB hB_eq using hA
+    refine ⟨fun n ↦ B (Nat.unpair n).1 (Nat.unpair n).2, fun _ ↦ hB _ _, ?_⟩
+    simp [iInf_unpair, ← hB_eq])
+  (by
+    rintro s₁ s₂ hs h₂ _ ⟨t, ht, rfl⟩
+    exact h₂.iInf_mem fun n ↦ hs (ht n))
+
+attribute [to_dual existing] countableSupClosure
+
+@[to_dual]
+lemma mem_countableSupClosure_iff :
+    a ∈ countableSupClosure s ↔ ∃ (t : ℕ → α), (∀ n, t n ∈ s) ∧ ⨆ n, t n = a := Iff.rfl
+
+@[to_dual (attr := simp)] lemma subset_countableSupClosure {s : Set α} :
+    s ⊆ countableSupClosure s := countableSupClosure.le_closure _
+
+@[to_dual (attr := simp)] lemma countableSupClosed_countableSupClosure :
+CountableSupClosed (countableSupClosure s) :=
+  countableSupClosure.isClosed_closure _
+
+@[to_dual (attr := simp)] lemma supClosed_countableSupClosure : SupClosed (countableSupClosure s) :=
+  countableSupClosed_countableSupClosure.supClosed
+
+@[to_dual]
+lemma countableSupClosure_mono : Monotone (countableSupClosure : Set α → Set α) :=
+  countableSupClosure.monotone
+
+@[to_dual (attr := simp)] lemma countableSupClosure_eq_self :
+    countableSupClosure s = s ↔ CountableSupClosed s :=
+  countableSupClosure.isClosed_iff.symm
+
+@[to_dual]
+alias ⟨_, CountableSupClosed.countableSupClosure_eq⟩ := countableSupClosure_eq_self
+
+@[to_dual]
+lemma countableSupClosure_idem (s : Set α) : countableSupClosure (countableSupClosure s) =
+    countableSupClosure s :=
+  countableSupClosure.idempotent _
+
+@[to_dual (attr := simp)] lemma countableSupClosure_singleton_bot :
+    countableSupClosure {(⊥ : α)} = {⊥} := by simp
+
+@[to_dual (attr := simp)] lemma countableSupClosure_univ :
+    countableSupClosure (Set.univ : Set α) = Set.univ := by simp
+
+@[to_dual (attr := simp)] lemma upperBounds_countableSupClosure (s : Set α) :
+    upperBounds (countableSupClosure s) = upperBounds s :=
+  (upperBounds_mono_set subset_countableSupClosure).antisymm <| by
+    rintro a ha _ ⟨t, ht, rfl⟩
+    exact iSup_le fun n ↦ ha (ht n)
+
+@[to_dual (attr := simp)] lemma isLUB_countableSupClosure :
+    IsLUB (countableSupClosure s) a ↔ IsLUB s a := by simp [IsLUB]
+
+@[to_dual]
+lemma sup_mem_countableSupClosure (ha : a ∈ s) (hb : b ∈ s) : a ⊔ b ∈ countableSupClosure s :=
+  supClosed_countableSupClosure (subset_countableSupClosure ha) (subset_countableSupClosure hb)
+
+@[to_dual]
+lemma iSup_mem_countableSupClosure [Countable ι] [Nonempty ι] {A : ι → α} (hA : ∀ n, A n ∈ s) :
+    (⨆ n, A n) ∈ countableSupClosure s :=
+  countableSupClosed_countableSupClosure.iSup_mem (fun n ↦ subset_countableSupClosure (hA n))
+
+@[to_dual]
+lemma finsetSup'_mem_countableSupClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α}
+    (hf : ∀ i ∈ t, f i ∈ s) : t.sup' ht f ∈ countableSupClosure s :=
+  supClosed_countableSupClosure.finsetSup'_mem _ fun _i hi ↦ subset_countableSupClosure <| hf _ hi
+
+@[to_dual countableInfClosure_min]
+lemma countableSupClosure_min : s ⊆ t → CountableSupClosed t → countableSupClosure s ⊆ t :=
+  countableSupClosure.closure_min
+
+@[to_dual (attr := simp)] lemma countableSupClosure_prod (s : Set α) (t : Set β) :
+    countableSupClosure (s ×ˢ t) = countableSupClosure s ×ˢ countableSupClosure t :=
+  le_antisymm (countableSupClosure_min
+    (Set.prod_mono subset_countableSupClosure subset_countableSupClosure) <|
+    countableSupClosed_countableSupClosure.prod countableSupClosed_countableSupClosure) <| by
+      rintro ⟨_, _⟩ ⟨⟨u, hu, rfl⟩, v, hv, rfl⟩
+      exact ⟨fun n ↦ (u n, v n), fun n ↦ ⟨hu n, hv n⟩, by rw [Prod.iSup_mk]⟩
+
+end CompleteLattice
+
+section Frame
+
+/-- If a set is closed under binary suprema, then its countable infimum closure is also closed under
+binary suprema. -/
+protected lemma SupClosed.countableInfClosure [Order.Coframe α] (hs : SupClosed s) :
+    SupClosed (countableInfClosure s) := by
+  rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
+  rw [iInf_sup_iInf]
+  refine ⟨fun n ↦ t (Nat.unpair n).1 ⊔ u (Nat.unpair n).2, fun n ↦ ?_, ?_⟩
+  · simp only
+    exact hs (ht (Nat.unpair n).1) (hu (Nat.unpair n).2)
+  · rw [iInf_unpair (f := (fun n m ↦ t n ⊔ u m)), iInf_prod']
+
+/-- If a set is closed under binary infima, then its countable supremum closure is also closed under
+binary infima. -/
+@[to_dual existing]
+protected lemma InfClosed.countableSupClosure [Order.Frame α] (hs : InfClosed s) :
+    InfClosed (countableSupClosure s) := by
+  rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
+  rw [iSup_inf_iSup]
+  refine ⟨fun n ↦ t (Nat.unpair n).1 ⊓ u (Nat.unpair n).2, fun n ↦ ?_, ?_⟩
+  · simp only
+    exact hs (ht (Nat.unpair n).1) (hu (Nat.unpair n).2)
+  · rw [iSup_unpair (f := (fun n m ↦ t n ⊓ u m)), iSup_prod']
+
+attribute [to_dual existing] SupClosed.countableInfClosure
+
+end Frame
diff --git a/Mathlib/Order/SupClosed.lean b/Mathlib/Order/SupClosed.lean
index 8a640209feabd3..6771432d60a1c2 100644
--- a/Mathlib/Order/SupClosed.lean
+++ b/Mathlib/Order/SupClosed.lean
@@ -44,51 +44,64 @@ variable {ι : Sort*} {S : Set (Set α)} {f : ι → Set α} {s t : Set α} {a :
 open Set
 
 /-- A set `s` is *sup-closed* if `a ⊔ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
+@[to_dual /-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/]
 def SupClosed (s : Set α) : Prop := ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊔ b ∈ s
 
-@[simp] lemma supClosed_empty : SupClosed (∅ : Set α) := by simp [SupClosed]
-@[simp] lemma supClosed_singleton : SupClosed ({a} : Set α) := by simp [SupClosed]
+@[to_dual (attr := simp)] lemma supClosed_empty : SupClosed (∅ : Set α) := by simp [SupClosed]
+@[to_dual (attr := simp)] lemma supClosed_singleton : SupClosed ({a} : Set α) := by simp [SupClosed]
 
-@[simp] lemma supClosed_univ : SupClosed (univ : Set α) := by simp [SupClosed]
+@[to_dual (attr := simp)] lemma supClosed_univ : SupClosed (univ : Set α) := by simp [SupClosed]
+
+@[to_dual]
 lemma SupClosed.inter (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ∩ t) :=
   fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
 
+@[to_dual]
 lemma supClosed_sInter (hS : ∀ s ∈ S, SupClosed s) : SupClosed (⋂₀ S) :=
   fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)
 
+@[to_dual]
 lemma supClosed_iInter (hf : ∀ i, SupClosed (f i)) : SupClosed (⋂ i, f i) :=
   supClosed_sInter <| forall_mem_range.2 hf
 
 lemma SupClosed.directedOn (hs : SupClosed s) : DirectedOn (· ≤ ·) s :=
   fun _a ha _b hb ↦ ⟨_, hs ha hb, le_sup_left, le_sup_right⟩
 
+@[to_dual]
 lemma IsUpperSet.supClosed (hs : IsUpperSet s) : SupClosed s := fun _a _ _b ↦ hs le_sup_right
 
+@[to_dual]
 lemma SupClosed.preimage [FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) :
     SupClosed (f ⁻¹' s) :=
   fun a ha b hb ↦ by simpa [map_sup] using hs ha hb
 
+@[to_dual]
 lemma SupClosed.image [FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) :
     SupClosed (f '' s) := by
   rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
   rw [← map_sup]
   exact Set.mem_image_of_mem _ <| hs ha hb
 
+@[to_dual]
 lemma supClosed_range [FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range f) := by
   simpa using supClosed_univ.image f
 
+@[to_dual]
 lemma SupClosed.prod {t : Set β} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ×ˢ t) :=
   fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
 
+@[to_dual]
 lemma supClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeSup (α i)] {s : Set ι}
     {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, SupClosed (t i)) : SupClosed (s.pi t) :=
   fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
 
+@[to_dual]
 lemma SupClosed.insert_upperBounds {s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) :
     SupClosed (insert a s) := by
   rw [SupClosed]
   aesop
 
+@[to_dual]
 lemma SupClosed.insert_lowerBounds {s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) :
     SupClosed (insert a s) := by
   rw [SupClosed]
@@ -101,10 +114,12 @@ section Finset
 variable {ι : Type*} {f : ι → α} {s : Set α} {t : Finset ι} {a : α}
 open Finset
 
+@[to_dual]
 lemma SupClosed.finsetSup'_mem (hs : SupClosed s) (ht : t.Nonempty) :
     (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s :=
   sup'_induction _ _ hs
 
+@[to_dual]
 lemma SupClosed.finsetSup_mem [OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) :
     (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s :=
   sup'_eq_sup ht f ▸ hs.finsetSup'_mem ht
@@ -117,75 +132,12 @@ variable [SemilatticeInf α] [SemilatticeInf β]
 
 section Set
 variable {ι : Sort*} {S : Set (Set α)} {f : ι → Set α} {s t : Set α} {a : α}
-open Set
-
-/-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
-def InfClosed (s : Set α) : Prop := ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊓ b ∈ s
-
-@[simp] lemma infClosed_empty : InfClosed (∅ : Set α) := by simp [InfClosed]
-@[simp] lemma infClosed_singleton : InfClosed ({a} : Set α) := by simp [InfClosed]
-
-@[simp] lemma infClosed_univ : InfClosed (univ : Set α) := by simp [InfClosed]
-lemma InfClosed.inter (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ∩ t) :=
-  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
-
-lemma infClosed_sInter (hS : ∀ s ∈ S, InfClosed s) : InfClosed (⋂₀ S) :=
-  fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)
-
-lemma infClosed_iInter (hf : ∀ i, InfClosed (f i)) : InfClosed (⋂ i, f i) :=
-  infClosed_sInter <| forall_mem_range.2 hf
 
 lemma InfClosed.codirectedOn (hs : InfClosed s) : DirectedOn (· ≥ ·) s :=
   fun _a ha _b hb ↦ ⟨_, hs ha hb, inf_le_left, inf_le_right⟩
 
-lemma IsLowerSet.infClosed (hs : IsLowerSet s) : InfClosed s := fun _a _ _b ↦ hs inf_le_right
-
-lemma InfClosed.preimage [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) :
-    InfClosed (f ⁻¹' s) :=
-  fun a ha b hb ↦ by simpa [map_inf] using hs ha hb
-
-lemma InfClosed.image [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) :
-    InfClosed (f '' s) := by
-  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
-  rw [← map_inf]
-  exact Set.mem_image_of_mem _ <| hs ha hb
-
-lemma infClosed_range [FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range f) := by
-  simpa using infClosed_univ.image f
-
-lemma InfClosed.prod {t : Set β} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ×ˢ t) :=
-  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
-
-lemma infClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeInf (α i)] {s : Set ι}
-    {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, InfClosed (t i)) : InfClosed (s.pi t) :=
-  fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
-
-lemma InfClosed.insert_upperBounds {s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ upperBounds s) :
-    InfClosed (insert a s) := by
-  rw [InfClosed]
-  have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a
-  aesop
-
-lemma InfClosed.insert_lowerBounds {s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ lowerBounds s) :
-    InfClosed (insert a s) := by
-  rw [InfClosed]
-  aesop
-
 end Set
 
-section Finset
-variable {ι : Type*} {f : ι → α} {s : Set α} {t : Finset ι} {a : α}
-open Finset
-
-lemma InfClosed.finsetInf'_mem (hs : InfClosed s) (ht : t.Nonempty) :
-    (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s :=
-  inf'_induction _ _ hs
-
-lemma InfClosed.finsetInf_mem [OrderTop α] (hs : InfClosed s) (ht : t.Nonempty) :
-    (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s :=
-  inf'_eq_inf ht f ▸ hs.finsetInf'_mem ht
-
-end Finset
 end SemilatticeInf
 
 open Finset OrderDual