Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.opens.coe_bot

Modification history

2022-07-17 02:10

src/topology/sets/opens.lean

feat(topology/noetherian_space): Noetherian spaces (#14965)

Modified topological_space.opens.coe_bot View on Github →

2021-12-27 16:46

src/topology/opens.lean

feat(algebraic_geometry): Basic open set is empty iff section is zero in reduced schemes. (#11012)

Added topological_space.opens.coe_bot View on Github →