Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-23 06:00 b77916db

View on Github →

feat(algebraic_geometry/Scheme): improve cosmetics of definition (#7325) Purely cosmetic, but the definition is going on a poster, so ...

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

Modified src/algebraic_geometry/presheafed_space.lean

Modified src/topology/category/Top/open_nhds.lean

added theorem topological_space.open_nhds.open_embedding

Modified src/topology/category/Top/opens.lean

deleted theorem topological_space.opens.inclusion_open_embedding

added theorem topological_space.opens.open_embedding