∀ {X Y : AlgebraicGeometry.Scheme} {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
      U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f →
        AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)