α✝ : Type ?u.192359
β✝ : Type ?u.192362
γ : Type ?u.192365
ι : Type ?u.192368
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ limsup u f ≤ b
α✝ : Type ?u.192359
β✝ : Type ?u.192362
γ : Type ?u.192365
ι : Type ?u.192368
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x
contrapose! h
α✝ : Type ?u.192359
β✝ : Type ?u.192362
γ : Type ?u.192365
ι : Type ?u.192368
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ ∀ᶠ (n : β) in map u f, n ≤ b
α✝ : Type ?u.192359
β✝ : Type ?u.192362
γ : Type ?u.192365
ι : Type ?u.192368
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ limsup u f ≤ b
apply limsSup_le_of_le hu
no goals
α✝ : Type ?u.192359
β✝ : Type ?u.192362
γ : Type ?u.192365
ι : Type ?u.192368
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ ∀ᶠ (n : β) in map u f, n ≤ b
simpa using h