α : Type u_1
β : Type ?u.77846
γ : Type ?u.77849
ι : Type ?u.77852
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ sInf {a | ∀ (x : α), x ∈ s → x ≤ a} = sSup s
α : Type u_1
β : Type ?u.77846
γ : Type ?u.77849
ι : Type ?u.77852
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ limsSup (𝓟 s) = sSup s
simp only [limsSup, eventually_principal]
no goals
α : Type u_1
β : Type ?u.77846
γ : Type ?u.77849
ι : Type ?u.77852
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ sInf {a | ∀ (x : α), x ∈ s → x ≤ a} = sSup s
exact csInf_upper_bounds_eq_csSup h hs