case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.142440
ι✝ : Sort x
ι : Type u_1
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
val✝ : Fintype ι
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
α : Type u
β : Type v
γ : Type w
δ : Type ?u.142440
ι✝ : Sort x
ι : Type u_1
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
cases nonempty_fintype ι
no goals
case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.142440
ι✝ : Sort x
ι : Type u_1
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
val✝ : Fintype ι
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
simpa only [Filter.Eventually, setOf_forall] using iInter_mem