case h
X : TopCat
U : Opens ↑X
⊢ ↑((map (inclusion U)).obj U) = ↑⊤
X : TopCat
U : Opens ↑X
⊢ (map (inclusion U)).obj U = ⊤
ext1
no goals
case h
X : TopCat
U : Opens ↑X
⊢ ↑((map (inclusion U)).obj U) = ↑⊤
exact Subtype.coe_preimage_self _