J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
⊢ c.pt.str = ⨆ (j : J), coinduced ((forget TopCat).map (c.ι.app j)) (F.obj j).str
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
⊢ c.pt.str = ⨆ (j : J), coinduced ((forget TopCat).map (c.ι.app j)) (F.obj j).str
let homeo := homeoOfIso (hc.coconePointUniqueUpToIso (colimitCoconeIsColimit F))
case a.h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
x✝ : Set ↑c.pt
⊢ IsOpen x✝ ↔ IsOpen x✝
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
⊢ c.pt.str = ⨆ (j : J), coinduced ((forget TopCat).map (c.ι.app j)) (F.obj j).str
ext
case a.h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
x✝ : Set ↑c.pt
⊢ IsOpen (↑(Homeomorph.symm homeo) ⁻¹' x✝) ↔ ∀ (i : J), IsOpen x✝
case a.h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
x✝ : Set ↑c.pt
⊢ IsOpen x✝ ↔ IsOpen x✝
refine' homeo.symm.isOpen_preimage.symm.trans (Iff.trans _ isOpen_iSup_iff.symm)
no goals
case a.h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
x✝ : Set ↑c.pt
⊢ IsOpen (↑(Homeomorph.symm homeo) ⁻¹' x✝) ↔ ∀ (i : J), IsOpen x✝
exact isOpen_iSup_iff