α : Type u_1
β : Type ?u.59735
γ : Type ?u.59738
ι : Sort u_2
κ : ι → Sort ?u.59746
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ (a ∈ ⋃ (i : ι), ↑(f i)) ↔ ∃ i, a ∈ f i
α : Type u_1
β : Type ?u.59735
γ : Type ?u.59738
ι : Sort u_2
κ : ι → Sort ?u.59746
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ (a ∈ ⨅ (i : ι), f i) ↔ ∃ i, a ∈ f i
rw [← SetLike.mem_coe, coe_iInf]
no goals
α : Type u_1
β : Type ?u.59735
γ : Type ?u.59738
ι : Sort u_2
κ : ι → Sort ?u.59746
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ (a ∈ ⋃ (i : ι), ↑(f i)) ↔ ∃ i, a ∈ f i
exact mem_iUnion