no goals
α : Type u_1
β : Type ?u.4511
ι : Sort ?u.4514
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∃ s, s ∈ l ∧ ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s, s ∈ l ∧ ∃ t, t ∈ l' ∧ ∀ (x : α), x ∈ t → x ∈ s → p x
simp only [eventually_iff_exists_mem]
no goals
α : Type u_1
β : Type ?u.4511
ι : Sort ?u.4514
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∃ s, s ∈ l ∧ ∃ t, t ∈ l' ∧ ∀ (x : α), x ∈ t → x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]