mathlib3
6d0f40a6 - chore(topology/algebra/ordered): use `continuous_at`, rename (#3231)

Commit
5 years ago
chore(topology/algebra/ordered): use `continuous_at`, rename (#3231) * rename `Sup_mem_of_is_closed` and `Inf_mem_of_is_closed` to `is_closed.Sup_mem` and `is_closed.Inf_mem`, similarly with `cSup` and `cInf`; * make `Sup_of_continuous` etc take `continuous_at` instead of `continuous`, rename to `Sup_of_continuous_at_of_monotone` etc, similarly with `cSup`/`cInf`.
Author
Parents
Loading