α : Type u_1
β : Type ?u.76667
γ : Type ?u.76670
ι : Sort u_2
κ : ι → Sort ?u.76678
inst✝ : LE α
S : Set (LowerSet α)
s t : LowerSet α
a : α
f : ι → LowerSet α
⊢ (a ∈ ⋃ (i : ι), ↑(f i)) ↔ ∃ i, a ∈ f i
α : Type u_1
β : Type ?u.76667
γ : Type ?u.76670
ι : Sort u_2
κ : ι → Sort ?u.76678
inst✝ : LE α
S : Set (LowerSet α)
s t : LowerSet α
a : α
f : ι → LowerSet α
⊢ (a ∈ ⨆ (i : ι), f i) ↔ ∃ i, a ∈ f i
rw [← SetLike.mem_coe, coe_iSup]
no goals
α : Type u_1
β : Type ?u.76667
γ : Type ?u.76670
ι : Sort u_2
κ : ι → Sort ?u.76678
inst✝ : LE α
S : Set (LowerSet α)
s t : LowerSet α
a : α
f : ι → LowerSet α
⊢ (a ∈ ⋃ (i : ι), ↑(f i)) ↔ ∃ i, a ∈ f i
exact mem_iUnion