simp [← biUnion_univ, hs.subset_biUnion_mono_iff directedOn_univ univ_nonempty hv]
α : Type u_1
s : Set α
ι : Type u_2
inst✝² : LE ι
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : Nonempty ι
v : ι → Set α
hs : s.Finite
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
⊢ s ⊆ ⋃ i, v i ↔ ∃ i, s ⊆ v i
no goals