mathlib
21415c8c
- chore(topology/algebra/ordered): drop section vars, golf 2 proofs (#4706)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(topology/algebra/ordered): drop section vars, golf 2 proofs (#4706) * Explicitly specify explicit arguments instead of using section variables; * Add `continuous_min` and `continuous_max`; * Use them for `tendsto.min` and `tendsto.max`
References
#4925 - Make prime-avoidance branch build
Author
urkud
Parents
0cf8a98b
Loading