α : Type u_2
f✝ : Filter α
β : Type u_1
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun a' => u a' i) f
α : Type u_2
f✝ : Filter α
β : Type u_1
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun a' => u a' b) f
rw [eventually_countable_forall]
no goals
α : Type u_2
f✝ : Filter α
β : Type u_1
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun a' => u a' i) f
exact fun b => ENNReal.eventually_le_limsup fun a => u a b