α : Type u_1
β : Type ?u.59414
γ : Type ?u.59417
ι : Sort u_2
κ : ι → Sort ?u.59425
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ (a ∈ ⋂ (i : ι), ↑(f i)) ↔ ∀ (i : ι), a ∈ f i
α : Type u_1
β : Type ?u.59414
γ : Type ?u.59417
ι : Sort u_2
κ : ι → Sort ?u.59425
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ (a ∈ ⨆ (i : ι), f i) ↔ ∀ (i : ι), a ∈ f i
rw [← SetLike.mem_coe, coe_iSup]
no goals
α : Type u_1
β : Type ?u.59414
γ : Type ?u.59417
ι : Sort u_2
κ : ι → Sort ?u.59425
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
f : ι → UpperSet α
⊢ (a ∈ ⋂ (i : ι), ↑(f i)) ↔ ∀ (i : ι), a ∈ f i
exact mem_iInter