simple_func_dense): distance to `approx_on` is antitone (#9271)

Commit

4 years ago

chore(measure_theory/function/simple_func_dense): distance to `approx_on` is antitone (#9271)

Author

urkud

Parents