case h
α : Type u
β : Type v
γ : Type w
δ : Type ?u.101230
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type u_1
f : ι → Filter α
⊢ Directed (fun x x_1 => x ≥ x_1) fun t => ⨅ (i : ι) (_ : i ∈ t), f i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.101230
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type u_1
f : ι → Filter α
⊢ (⨅ (i : ι), f i).sets = ⋃ (t : Finset ι), (⨅ (i : ι) (_ : i ∈ t), f i).sets
rw [iInf_eq_iInf_finset, iInf_sets_eq]
no goals
case h
α : Type u
β : Type v
γ : Type w
δ : Type ?u.101230
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type u_1
f : ι → Filter α
⊢ Directed (fun x x_1 => x ≥ x_1) fun t => ⨅ (i : ι) (_ : i ∈ t), f i
exact directed_of_sup fun _ _ => biInf_mono