α : Type u_1
β : Type ?u.60399
γ : Type ?u.60402
ι : Sort ?u.60405
ι' : Sort ?u.60408
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → Set.Nonempty (s ∩ s')) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U
α : Type u_1
β : Type ?u.60399
γ : Type ?u.60402
ι : Sort ?u.60405
ι' : Sort ?u.60408
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f g : Filter α
⊢ NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x
simp only [inf_neBot_iff, frequently_iff, and_comm]
no goals
α : Type u_1
β : Type ?u.60399
γ : Type ?u.60402
ι : Sort ?u.60405
ι' : Sort ?u.60408
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → Set.Nonempty (s ∩ s')) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U
rfl