@[simp]

theorem Nucleus.sSup_apply {X : Type u_1} [Order.Frame X] (s : Set (Nucleus X)) (x : X) : (sSup s) x = ⨅ j ∈ upperBounds s, j x

@[simp]

theorem Nucleus.iSup_apply {X : Type u_1} [Order.Frame X] (x : X) {ι : Type u_2} (f : ι → Nucleus X) : (iSup f) x = ⨅ j ∈ upperBounds (Set.range f), j x

@[simp]

theorem Nucleus.sup_apply {X : Type u_1} [Order.Frame X] (x : X) (m n : Nucleus X) : (m ⊔ n) x = ⨅ j ∈ upperBounds {m, n}, j x