case h
X : TopCat
U : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj ⊤) = ↑U
X : TopCat
U : Opens ↑X
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj ⊤ = U
ext1
no goals
case h
X : TopCat
U : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj ⊤) = ↑U
exact Set.image_univ.trans Subtype.range_coe