refactor(calculus): simplify derivative extension

[PatrickMassot]

This is the PR promised in the #1794 discussion. Sébastien used sequences to prove a derivative extension lemma. The main point of the current PR us to make sure the library allows a sequence-free proof. Recall the main lemma replacing the use of sequences in topology is

lemma image_closure_subset_closure_image {f : α → β} {s : set α} (h : continuous f) :
  f '' closure s ⊆ closure (f '' s)

from here. Here we need a version with weaker assumptions. This PR introduces:

lemma continuous_within_at.image_closure {f : α → β} {s : set α}
  (hf : ∀ x ∈ closure s, continuous_within_at f s x) :
  f '' (closure s) ⊆ closure (f '' s)

which is a tiny repackaging of an existing lemma. I also added a lemma about ordered topologies with similar weak assumptions:

lemma continuous_within_at.closure_le  {f g : β → α} {s : set β}
 (hf : ∀ x ∈ closure s, continuous_within_at f s x) (hg : ∀ x ∈ closure s, continuous_within_at g s x)
 (h : ∀ x ∈ s, f x ≤ g x) : ∀ x ∈ closure s, f x ≤ g x

for which I couldn't find a good name.
Using those two lemmas indeed simplifies the derivative extension main lemma (at least if you like that kind of proof).

[sgouezel]

To obtain f x ≤ g x at a given x in the closure of s, you only need the continuity of f and g at this specific x. So, I think a statement involving one fixed x and assumptions continuous_within_at f s x, continuous_within_at g s x and x ∈ closure s would be more natural.

[PatrickMassot]

Good point. I fixed that. But maybe I'm having too much fun with filters in the new proof...

[sgouezel]

I think you can take a shortcut by using continuous_within_at.mem_closure_image here. Possibly with the following version that could be worth adding just below continuous_within_at.mem_closure_image.

lemma continuous_within_at.mem_closure {f : α → β} {s : set α} {x : α} {A : set β}
  (h : continuous_within_at f s x) (hx : x ∈ closure s) (hA : s ⊆ f⁻¹' A) : f x ∈ closure A :=
closure_mono (image_subset_iff.2 hA) (h.mem_closure_image hx)

[PatrickMassot]

Nice! I've done it.

[urkud]

Do we have continuous_on.image_closure assuming is_closed s and continuous_on f s?

[PatrickMassot]

I don't think so.