Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 03:23 ea469516

View on Github →

feat(algebraic_geometry/open_immersion): is_open_immersion.lift_app (#17186)

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.hom.inv_app

modified def algebraic_geometry.Scheme.hom.opens_functor

added theorem algebraic_geometry.is_open_immersion.app_eq_inv_app_app_of_comp_eq

added theorem algebraic_geometry.is_open_immersion.app_eq_inv_app_app_of_comp_eq_aux

added theorem algebraic_geometry.is_open_immersion.lift_app