Commit 2020-02-08 13:25 bcb63ebf
View on Github →refactor(topology/*): irreducible and connected sets are nonempty (#1964)
- refactor(topology/*): irreducible and connected sets are nonempty
- Fix typos
- Fix more typos
- Update src/topology/subset_properties.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Update src/topology/subset_properties.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Refactor 'nonempty' fields
- Fix spacing in set-builder
- Use dot notation
- Write a comment on the nonempty assumption
- Apply suggestions from code review
- Fix build
- Tiny improvements