From 1f74ddd2266b9558f19a66b5dc2bef11416fd1a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Mon, 20 Jul 2020 20:30:53 +0000 Subject: [PATCH] feat(topology/local_extr): add lemmas on composition with continuous functions (#3459) --- src/topology/local_extr.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/topology/local_extr.lean b/src/topology/local_extr.lean index d70f0f2743f17..16bbecfc4b251 100644 --- a/src/topology/local_extr.lean +++ b/src/topology/local_extr.lean @@ -252,6 +252,24 @@ lemma is_local_extr.comp_continuous_on [topological_space δ] {s : set δ} (g : hf.elim (λ hf, (hf.comp_continuous_on hg hb).is_extr) (λ hf, (is_local_max.comp_continuous_on hf hg hb).is_extr) +lemma is_local_min_on.comp_continuous_on [topological_space δ] {t : set α} {s : set δ} {g : δ → α} {b : δ} + (hf : is_local_min_on f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : continuous_on g s) (hb : b ∈ s) : + is_local_min_on (f ∘ g) s b := +hf.comp_tendsto (tendsto_nhds_within_mono_right (image_subset_iff.mpr hst) + (continuous_within_at.tendsto_nhds_within_image (hg b hb))) + +lemma is_local_max_on.comp_continuous_on [topological_space δ] {t : set α} {s : set δ} {g : δ → α} {b : δ} + (hf : is_local_max_on f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : continuous_on g s) (hb : b ∈ s) : + is_local_max_on (f ∘ g) s b := +hf.comp_tendsto (tendsto_nhds_within_mono_right (image_subset_iff.mpr hst) + (continuous_within_at.tendsto_nhds_within_image (hg b hb))) + +lemma is_local_extr_on.comp_continuous_on [topological_space δ] {t : set α} {s : set δ} (g : δ → α) {b : δ} + (hf : is_local_extr_on f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : continuous_on g s) (hb : b ∈ s) : + is_local_extr_on (f ∘ g) s b := +hf.elim (λ hf, (hf.comp_continuous_on hst hg hb).is_extr) + (λ hf, (is_local_max_on.comp_continuous_on hf hst hg hb).is_extr) + end preorder /-! ### Pointwise addition -/