mathlib
a18680a6 - chore(topology/continuous_function/ordered): split from `continuous_function/basic` (#11761)

Commit
3 years ago
chore(topology/continuous_function/ordered): split from `continuous_function/basic` (#11761) Split material about orders out from `continuous_function/basic`, to move that file lower down the import hierarchy.
Author
Parents
Loading