ext
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ thickening v (thickening u s) = thickening (u ○ v) s
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
x✝ : α
⊢ x✝ ∈ thickening v (thickening u s) ↔ x✝ ∈ thickening (u ○ v) s