α : Type u_1
β : Type ?u.61014
γ : Type ?u.61017
ι : Sort ?u.61020
ι' : Sort ?u.61023
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f g : Filter α
⊢ NeBot (g ⊓ f) ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
α : Type u_1
β : Type ?u.61014
γ : Type ?u.61017
ι : Sort ?u.61020
ι' : Sort ?u.61023
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 g, p x) → ∃ᶠ (x : α) in f, p x
rw [inf_comm]
no goals
α : Type u_1
β : Type ?u.61014
γ : Type ?u.61017
ι : Sort ?u.61020
ι' : Sort ?u.61023
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f g : Filter α
⊢ NeBot (g ⊓ f) ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
exact inf_neBot_iff_frequently_left