case a.h
α : Type u_1
β : Type ?u.148351
γ : Type ?u.148354
ι : Sort ?u.148357
κ : ι → Sort ?u.148362
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
x : α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨆ (a : α) (_ : a ∈ s), Iic a) ↔ x✝ ∈ ↑(lowerClosure s)
α : Type u_1
β : Type ?u.148351
γ : Type ?u.148354
ι : Sort ?u.148357
κ : ι → Sort ?u.148362
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
x : α
s : Set α
⊢ (⨆ (a : α) (_ : a ∈ s), Iic a) = lowerClosure s
ext
no goals
case a.h
α : Type u_1
β : Type ?u.148351
γ : Type ?u.148354
ι : Sort ?u.148357
κ : ι → Sort ?u.148362
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
x : α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨆ (a : α) (_ : a ∈ s), Iic a) ↔ x✝ ∈ ↑(lowerClosure s)
simp