Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-25 05:09 0dd60aeb

View on Github →

feat(algebraic_geometry): Schemes are sober. (#11040) Also renamed things in topology/sober.lean.

Estimated changes

Modified src/algebraic_geometry/properties.lean

Modified src/topology/sober.lean

added theorem closed_embedding.quasi_sober

deleted theorem closed_embedding.sober

added theorem open_embedding.quasi_sober

deleted theorem open_embedding.sober

added theorem quasi_sober_of_open_cover

deleted theorem sober_of_open_cover