Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-16 19:00 b7db5080

View on Github →

feat(analysis/topology/topological_space): basis elements are open

Estimated changes

Modified analysis/topology/topological_space.lean

added theorem topological_space.is_open_of_is_topological_basis

added theorem topological_space.mem_basis_subset_of_mem_open