case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑((map f).obj (iSup U)) = ↑(iSup ((map f).toPrefunctor.obj ∘ U))
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).toPrefunctor.obj ∘ U)
ext1
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑{ carrier := (forget TopCat).map f ⁻¹' ⋃ (i : ι), ↑(U i), is_open' := (_ : IsOpen (↑f ⁻¹' ⋃ (i : ι), ↑(U i))) } =
    ↑{ carrier := ⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i),
        is_open' := (_ : IsOpen (⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i))) }
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑((map f).obj (iSup U)) = ↑(iSup ((map f).toPrefunctor.obj ∘ U))
rw [iSup_def, iSup_def, map_obj]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ((forget TopCat).map f ⁻¹' ⋃ (i : ι), ↑(U i)) = ⋃ (i : ι), ↑((map f).obj (U i))
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑{ carrier := (forget TopCat).map f ⁻¹' ⋃ (i : ι), ↑(U i), is_open' := (_ : IsOpen (↑f ⁻¹' ⋃ (i : ι), ↑(U i))) } =
    ↑{ carrier := ⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i),
        is_open' := (_ : IsOpen (⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i))) }
dsimp
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (⋃ (i : ι), (forget TopCat).map f ⁻¹' ↑(U i)) = ⋃ (i : ι), ↑((map f).obj (U i))
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ((forget TopCat).map f ⁻¹' ⋃ (i : ι), ↑(U i)) = ⋃ (i : ι), ↑((map f).obj (U i))
rw [Set.preimage_iUnion]
no goals
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (⋃ (i : ι), (forget TopCat).map f ⁻¹' ↑(U i)) = ⋃ (i : ι), ↑((map f).obj (U i))
rfl