monotone_on.mono

Stream: Is there code for X?

[Sebastien Gouezel]

Do we really not have this?

lemma monotone_on.mono (f : ℝ → ℝ) (s t : set ℝ) (hf : monotone_on f s) (h : t ⊆ s) : monotone_on f t :=
by library_search

fails for me (but maybe I don't have the right imports).

[Sebastien Gouezel]

#13863

[Patrick Massot]

Importing all of mathlib is not enough

[Patrick Massot]

Quick reminder everyone: leanproject mk-all will create for you a file all.lean in src importing every file from your project (for instance mathlib). You can then type import all in a scratch file and run library_search there.

[Kevin Buzzard]

If library_search fails, how do we tell if something timed out or if it just wasn't there?

[Scott Morrison]

You'll get a deterministic timeout if library_search times out, otherwise a message saying it didn't find anything, and suggesting you try library_search!.

[Alex J. Best]

You can always bump up the time out temporarily, https://leanprover-community.github.io/tips_and_tricks.html#memory-and-deterministic-timeout