no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.97618
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s
ne : Set.Nonempty s
t : Set α
⊢ t ∈ (⨅ (i : β) (_ : i ∈ s), f i).sets ↔ t ∈ ⋃ (i : β) (_ : i ∈ s), (f i).sets
simp [mem_biInf_of_directed h ne]