case h
X : TopCat
U V : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj ((map (inclusion U)).obj V)) = ↑(V ⊓ U)
X : TopCat
U V : Opens ↑X
⊢ (IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj ((map (inclusion U)).obj V) = V ⊓ U
ext1
case h
X : TopCat
U V : Opens ↑X
⊢ (V.1 ∩ Set.range fun x => (forget TopCat).map (inclusion U) x) = ↑(V ⊓ U)
case h
X : TopCat
U V : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ((forget TopCat).map (inclusion U)))).obj ((map (inclusion U)).obj V)) = ↑(V ⊓ U)
refine' Set.image_preimage_eq_inter_range.trans _
case h
X : TopCat
U V : Opens ↑X
⊢ V.1 ∩ ↑U = ↑(V ⊓ U)
case h
X : TopCat
U V : Opens ↑X
⊢ (V.1 ∩ Set.range fun x => (forget TopCat).map (inclusion U) x) = ↑(V ⊓ U)
rw [set_range_forget_map_inclusion U]
no goals
case h
X : TopCat
U V : Opens ↑X
⊢ V.1 ∩ ↑U = ↑(V ⊓ U)
rfl