Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes