α : Type u_2
β : Type u_1
γ : Type ?u.102493
ι : Type ?u.102496
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
α : Type u_2
β : Type u_1
γ : Type ?u.102493
ι : Type ?u.102496
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x => ⊥) f = ⊥
rw [limsup_eq, eq_bot_iff]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.102493
ι : Type ?u.102496
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
exact sInf_le (eventually_of_forall fun _ => le_rfl)