∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens),
  Set.range ⇑(CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f) = Set.range ⇑U.ι