α : Type u_2
β : Type u_3
γ : Type ?u.25296
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x x_1 => x ≥ x_1) f
hg : Monotone g
s : Set β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ (i : ι), Filter.lift (f i) g
α : Type u_2
β : Type u_3
γ : Type ?u.25296
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x x_1 => x ≥ x_1) f
hg : Monotone g
s : Set β
⊢ s ∈ Filter.lift (iInf f) g → s ∈ ⨅ (i : ι), Filter.lift (f i) g
simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.25296
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x x_1 => x ≥ x_1) f
hg : Monotone g
s : Set β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ (i : ι), Filter.lift (f i) g
exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs