α : Type u_1
β : Type ?u.185642
γ : Type ?u.185645
ι : Type ?u.185648
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ¬∃ᶠ (n : α) in f, a < n
⊢ limsSup f ≤ a
α : Type u_1
β : Type ?u.185642
γ : Type ?u.185645
ι : Type ?u.185648
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : a < limsSup f
⊢ ∃ᶠ (n : α) in f, a < n
contrapose! h
α : Type u_1
β : Type ?u.185642
γ : Type ?u.185645
ι : Type ?u.185648
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ limsSup f ≤ a
α : Type u_1
β : Type ?u.185642
γ : Type ?u.185645
ι : Type ?u.185648
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ¬∃ᶠ (n : α) in f, a < n
⊢ limsSup f ≤ a
simp only [not_frequently, not_lt] at h
no goals
α : Type u_1
β : Type ?u.185642
γ : Type ?u.185645
ι : Type ?u.185648
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ limsSup f ≤ a
exact limsSup_le_of_le hf h