no goals
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
f : ι → α
a : α
⊢ (⋃ (i : ι), Ico (f i) a) = Iio a ↔ ∀ (x : α), x < a → ∃ i, f i ≤ x
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]