α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ (∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f
α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu_le : ∃ᶠ (x : α) in f, b ≤ u x
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ b ≤ limsup u f
revert hu_le
α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ ¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x
α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ (∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f
rw [← not_imp_not, not_frequently]
α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ limsup u f < b → ∀ᶠ (x : α) in f, u x < b
α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ ¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x
simp_rw [← lt_iff_not_ge]
no goals
α✝ : Type ?u.190748
β✝ : Type ?u.190751
γ : Type ?u.190754
ι : Type ?u.190757
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ limsup u f < b → ∀ᶠ (x : α) in f, u x < b
exact fun h => eventually_lt_of_limsup_lt h hu