[Merged by Bors] - feat(Order/Nucleus): nuclei form a complete lattice

Mathlib/Order/Nucleus.lean

@@ -111,4 +111,33 @@ instance : BoundedOrder (Nucleus X) where
   bot_le _ _ := le_apply
   le_top _ _ := by simp
 
+instance : InfSet (Nucleus X) where
+  sInf s :=
+  { toFun x := ⨅ f ∈ s, f x,
+    map_inf' x y := by
+      simp only [InfHomClass.map_inf, le_antisymm_iff, le_inf_iff, le_iInf_iff]
+      refine ⟨⟨?_, ?_⟩, ?_⟩ <;> rintro f hf
+      · exact iInf₂_le_of_le f hf inf_le_left
+      · exact iInf₂_le_of_le f hf inf_le_right
+      · exact ⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩
+    idempotent' x := by
+      simp only [le_iInf_iff, iInf_le_iff]
+      intro a ha b h
+      rw [← idempotent]
+      apply le_trans (h a ha)
+      gcongr
+      simp_all [iInf_le_iff]
+    le_apply' x := by simp [le_apply]}
+
+theorem sInf_apply (s : Set (Nucleus X)) (x : X) : sInf s x = ⨅ j ∈ s, j x := rfl
+
+theorem iInf_apply {ι : Type*} (s : ι → (Nucleus X)) (x : X) :
+    iInf s x = ⨅ j ∈ Set.range s, j x := by simp [iInf, sInf_apply]
+
+instance : CompleteSemilatticeInf (Nucleus X) where
+  sInf_le := (by simp_all [LE.le, sInf_apply, iInf_le_iff])
+  le_sInf := (by simp_all [LE.le, sInf_apply])
+
+instance : CompleteLattice (Nucleus X) := completeLatticeOfCompleteSemilatticeInf (Nucleus X)
+
 end Nucleus