mathlib3
ec11e5f5 - feat(algebra/covariant_and_contravariant): covariance and monotonicity (#11815)

Commit
4 years ago
feat(algebra/covariant_and_contravariant): covariance and monotonicity (#11815) Some simple lemmas about monotonicity and covariant operators. Proves things like `monotone f → monotone (λ n, f (3 + n))` by library search.
Parents
Loading