feat(Topology/Continuous): continuous iff f '' closure s ⊆ closure (f '' s) or f ⁻¹' (interior s) ⊆ interior (f ⁻¹' s) (leanprover-community#34395)

Author: SnirBroshi

Mathlib/Topology/Continuous.lean

@@ -97,6 +97,11 @@ theorem preimage_interior_subset_interior_preimage {t : Set Y} (hf : Continuous
     f ⁻¹' interior t ⊆ interior (f ⁻¹' t) :=
   interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf)
 
+theorem continuous_iff_preimage_interior_subset_interior_preimage :
+    Continuous f ↔ ∀ s, f ⁻¹' (interior s) ⊆ interior (f ⁻¹' s) where
+  mp h s := preimage_interior_subset_interior_preimage h
+  mpr h := ⟨fun s hs ↦ subset_interior_iff_isOpen.mp <| by grw [← h, hs.interior_eq]⟩
+
 @[continuity]
 theorem continuous_id : Continuous (id : X → X) :=
   continuous_def.2 fun _ => id
@@ -217,6 +222,12 @@ theorem closure_subset_preimage_closure_image (h : Continuous f) :
     closure s ⊆ f ⁻¹' closure (f '' s) :=
   (mapsTo_image _ _).closure h
 
+theorem continuous_iff_image_closure_subset_closure_image :
+    Continuous f ↔ ∀ s, f '' closure s ⊆ closure (f '' s) where
+  mp h s := image_closure_subset_closure_image h
+  mpr h := continuous_iff_isClosed.mpr fun s hs ↦ isClosed_of_closure_subset <| by
+    grw [image_subset_iff.mp <| h <| f ⁻¹' s, image_preimage_subset, hs.closure_subset]
+
 theorem map_mem_closure {t : Set Y} (hf : Continuous f)
     (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t :=
   ht.closure hf hx