α : Type u_1
β : Type ?u.19100
γ : Type ?u.19103
ι : Sort u_2
ι' : Sort ?u.19109
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x
α : Type u_1
β : Type ?u.19100
γ : Type ?u.19103
ι : Sort u_2
ι' : Sort ?u.19109
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
q : α → Prop
⊢ (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x
simp only [Filter.Frequently, hl.eventually_iff]
α : Type u_1
β : Type ?u.19100
γ : Type ?u.19103
ι : Sort u_2
ι' : Sort ?u.19109
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
q : α → Prop
⊢ (∀ (i : ι), p i → Exists fun ⦃x⦄ => x ∈ s i ∧ q x) ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x
α : Type u_1
β : Type ?u.19100
γ : Type ?u.19103
ι : Sort u_2
ι' : Sort ?u.19109
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x
push_neg
no goals
α : Type u_1
β : Type ?u.19100
γ : Type ?u.19103
ι : Sort u_2
ι' : Sort ?u.19109
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
q : α → Prop
⊢ (∀ (i : ι), p i → Exists fun ⦃x⦄ => x ∈ s i ∧ q x) ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x
rfl