α : Type u
β : Type v
γ : Type w
δ : Type ?u.161008
ι : Sort x
f : Filter α
P : α → Prop
⊢ (∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, q x ∧ P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x, x ∈ U ∧ P x
α : Type u
β : Type v
γ : Type w
δ : Type ?u.161008
ι : Sort x
f : Filter α
P : α → Prop
⊢ (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x, x ∈ U ∧ P x
simp only [frequently_iff_forall_eventually_exists_and, exists_prop, @and_comm (P _)]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.161008
ι : Sort x
f : Filter α
P : α → Prop
⊢ (∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, q x ∧ P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x, x ∈ U ∧ P x
rfl