Commit 2019-12-28 13:01 e43905be
View on Github →refactor(topology/algebra/ordered): formulate a few "Icc induction" principles (#1833)
- refactor(topology/algebra/ordered): use
tfae, prove equality of somenhds_within - Add missing
order_dual.*instances - Try to fix the build
- Fix formatting, rename some variables
- refactor(topology/algebra/ordered): formulate a few "Icc induction" principles
They have other applications than proving
is_connected_Icc. - Fix doc Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Rephraze docs
- Drop an unused argument