Commit 2020-02-11 09:25 4e2c7e36
View on Github →feat(topology/subset_properties): alternative definitions of irreducible and connected (#1970)
- 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
- irreducible_iff statements
- Fix build
- Tiny improvements
- Justify that connected spaces are nonempty
- Add docstrings
- Update src/topology/subset_properties.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Update subset_properties.lean