From cc3c28280191fdd42f5b4983c86e40ec6f253dd2 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 16 Aug 2023 19:05:03 +0300 Subject: [PATCH 1/3] feat: two missing lemmas about restricting continuous maps --- Mathlib/Topology/Constructions.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 1cc532934424d..9656f12525048 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -1123,6 +1123,14 @@ theorem Continuous.codRestrict {f : α → β} {s : Set β} (hf : Continuous f) hf.subtype_mk hs #align continuous.cod_restrict Continuous.codRestrict +theorem Continuous.restrict {f : α → β} {s : Set α} {t : Set β} (h1 : MapsTo f s t) + (h2 : Continuous f) : Continuous (h1.restrict f s t) := + (h2.comp continuous_subtype_val).codRestrict _ + +theorem Continuous.restrictPreimage {f : α → β} {s : Set β} (h : Continuous f) : + Continuous (s.restrictPreimage f) := + h.restrict _ + theorem Inducing.codRestrict {e : α → β} (he : Inducing e) {s : Set β} (hs : ∀ x, e x ∈ s) : Inducing (codRestrict e s hs) := inducing_of_inducing_compose (he.continuous.codRestrict hs) continuous_subtype_val he From 2176efe24a0d3ec3a328abb726a9fd7f0bc6b073 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 16 Aug 2023 19:09:33 +0300 Subject: [PATCH 2/3] Golf --- Mathlib/Topology/Constructions.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 9656f12525048..fe1930d37f355 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -1100,8 +1100,8 @@ theorem closure_subtype {x : { a // p a }} {s : Set { a // p a }} : #align closure_subtype closure_subtype theorem continuousAt_codRestrict_iff {f : α → β} {t : Set β} (h1 : ∀ x, f x ∈ t) {x : α} : - ContinuousAt (codRestrict f t h1) x ↔ ContinuousAt f x := by - simp_rw [inducing_subtype_val.continuousAt_iff, Function.comp, val_codRestrict_apply] + ContinuousAt (codRestrict f t h1) x ↔ ContinuousAt f x := + inducing_subtype_val.continuousAt_iff #align continuous_at_cod_restrict_iff continuousAt_codRestrict_iff alias continuousAt_codRestrict_iff ↔ _ ContinuousAt.codRestrict From ff8998624882ec026cb83b1605f5ba848004b199 Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Sat, 19 Aug 2023 13:26:47 +0200 Subject: [PATCH 3/3] Apply suggestions from code review Co-authored-by: Oliver Nash --- Mathlib/Topology/Constructions.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index fe1930d37f355..191771d581d19 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -1099,6 +1099,7 @@ theorem closure_subtype {x : { a // p a }} {s : Set { a // p a }} : closure_induced #align closure_subtype closure_subtype +@[simp] theorem continuousAt_codRestrict_iff {f : α → β} {t : Set β} (h1 : ∀ x, f x ∈ t) {x : α} : ContinuousAt (codRestrict f t h1) x ↔ ContinuousAt f x := inducing_subtype_val.continuousAt_iff @@ -1123,10 +1124,12 @@ theorem Continuous.codRestrict {f : α → β} {s : Set β} (hf : Continuous f) hf.subtype_mk hs #align continuous.cod_restrict Continuous.codRestrict +@[continuity] theorem Continuous.restrict {f : α → β} {s : Set α} {t : Set β} (h1 : MapsTo f s t) (h2 : Continuous f) : Continuous (h1.restrict f s t) := (h2.comp continuous_subtype_val).codRestrict _ +@[continuity] theorem Continuous.restrictPreimage {f : α → β} {s : Set β} (h : Continuous f) : Continuous (s.restrictPreimage f) := h.restrict _