feat(analysis/normed_space/weak_dual): add the rest of Banach-Alaoglu…

… theorem (#9862)

The second of two parts to add the Banach-Alaoglu theorem about the compactness of the closed unit ball (and more generally polar sets of neighborhoods of the origin) of the dual of a normed space in the weak-star topology.

This second half is about the embedding of the weak dual of a normed space into a (big) product of the ground fields, and the required compactness statements from Tychonoff's theorem. In particular it contains the actual Banach-Alaoglu theorem.

Co-Authored-By: Yury Kudryashov <urkud@urkud.name>



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

src/analysis/normed_space/dual.lean

@@ -142,11 +142,11 @@ open metric set normed_space
 `polar 𝕜 s` is the subset of `dual 𝕜 E` consisting of those functionals which
 evaluate to something of norm at most one at all points `z ∈ s`. -/
 def polar (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E] : set E → set (dual 𝕜 E) :=
+  {E : Type*} [semi_normed_group E] [normed_space 𝕜 E] : set E → set (dual 𝕜 E) :=
 (dual_pairing 𝕜 E).flip.polar
 
 variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
-variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables {E : Type*} [semi_normed_group E] [normed_space 𝕜 E]
 
 lemma mem_polar_iff {x' : dual 𝕜 E} (s : set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ∥x' z∥ ≤ 1 := iff.rfl
 

src/analysis/normed_space/operator_norm.lean

@@ -1357,7 +1357,7 @@ that it belongs to the closure of the image of a bounded set `s : set (E →SL[
 to function. Coercion to function of the result is definitionally equal to `f`. -/
 @[simps apply { fully_applied := ff }]
 def of_mem_closure_image_coe_bounded (f : E' → F) {s : set (E' →SL[σ₁₂] F)} (hs : bounded s)
-  (hf : f ∈ closure ((λ g x, g x : (E' →SL[σ₁₂] F) → E' → F) '' s)) :
+  (hf : f ∈ closure ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s)) :
   E' →SL[σ₁₂] F :=
 begin
   -- `f` is a linear map due to `linear_map_of_mem_closure_range_coe`
@@ -1428,6 +1428,80 @@ begin
   exact ⟨Glin, tendsto_of_tendsto_pointwise_of_cauchy_seq (tendsto_pi_nhds.2 hG) hf⟩
 end
 
+/-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values
+in a proper space. Then `s` interpreted as a set in the space of maps `E → F` with topology of
+pointwise convergence is precompact: its closure is a compact set. -/
+lemma is_compact_closure_image_coe_of_bounded [proper_space F] {s : set (E' →SL[σ₁₂] F)}
+  (hb : bounded s) :
+  is_compact (closure ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s)) :=
+have ∀ x, is_compact (closure (apply' F σ₁₂ x '' s)),
+  from λ x, ((apply' F σ₁₂ x).lipschitz.bounded_image hb).is_compact_closure,
+compact_closure_of_subset_compact (is_compact_pi_infinite this)
+  (image_subset_iff.2 $ λ g hg x, subset_closure $ mem_image_of_mem _ hg)
+
+/-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values
+in a proper space. If `s` interpreted as a set in the space of maps `E → F` with topology of
+pointwise convergence is closed, then it is compact.
+
+TODO: reformulate this in terms of a type synonym with the right topology. -/
+lemma is_compact_image_coe_of_bounded_of_closed_image [proper_space F] {s : set (E' →SL[σ₁₂] F)}
+  (hb : bounded s) (hc : is_closed ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s)) :
+  is_compact ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s) :=
+hc.closure_eq ▸ is_compact_closure_image_coe_of_bounded hb
+
+/-- If a set `s` of semilinear functions is bounded and is closed in the weak-* topology, then its
+image under coercion to functions `E → F` is a closed set. We don't have a name for `E →SL[σ] F`
+with weak-* topology in `mathlib`, so we use an equivalent condition (see `is_closed_induced_iff'`).
+
+TODO: reformulate this in terms of a type synonym with the right topology. -/
+lemma is_closed_image_coe_of_bounded_of_weak_closed {s : set (E' →SL[σ₁₂] F)} (hb : bounded s)
+  (hc : ∀ f, (⇑f : E' → F) ∈ closure ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s) → f ∈ s) :
+  is_closed ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s) :=
+is_closed_of_closure_subset $ λ f hf,
+  ⟨of_mem_closure_image_coe_bounded f hb hf, hc (of_mem_closure_image_coe_bounded f hb hf) hf, rfl⟩
+
+/-- If a set `s` of semilinear functions is bounded and is closed in the weak-* topology, then its
+image under coercion to functions `E → F` is a compact set. We don't have a name for `E →SL[σ] F`
+with weak-* topology in `mathlib`, so we use an equivalent condition (see `is_closed_induced_iff'`).
+-/
+lemma is_compact_image_coe_of_bounded_of_weak_closed [proper_space F] {s : set (E' →SL[σ₁₂] F)}
+  (hb : bounded s)
+  (hc : ∀ f, (⇑f : E' → F) ∈ closure ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s) → f ∈ s) :
+  is_compact ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s) :=
+is_compact_image_coe_of_bounded_of_closed_image hb $
+  is_closed_image_coe_of_bounded_of_weak_closed hb hc
+
+/-- A closed ball is closed in the weak-* topology. We don't have a name for `E →SL[σ] F` with
+weak-* topology in `mathlib`, so we use an equivalent condition (see `is_closed_induced_iff'`). -/
+lemma is_weak_closed_closed_ball (f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄
+  (hf : ⇑f ∈ closure ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' (closed_ball f₀ r))) :
+  f ∈ closed_ball f₀ r :=
+begin
+  have hr : 0 ≤ r,
+    from nonempty_closed_ball.1 (nonempty_image_iff.1 (closure_nonempty_iff.1 ⟨_, hf⟩)),
+  refine mem_closed_ball_iff_norm.2 (op_norm_le_bound _ hr $ λ x, _),
+  have : is_closed {g : E' → F | ∥g x - f₀ x∥ ≤ r * ∥x∥},
+    from is_closed_Iic.preimage ((@continuous_apply E' (λ _, F) _ x).sub continuous_const).norm,
+  refine this.closure_subset_iff.2 (image_subset_iff.2 $ λ g hg, _) hf,
+  exact (g - f₀).le_of_op_norm_le (mem_closed_ball_iff_norm.1 hg) _
+end
+
+/-- The set of functions `f : E → F` that represent continuous linear maps `f : E →SL[σ₁₂] F`
+at distance `≤ r` from `f₀ : E →SL[σ₁₂] F` is closed in the topology of pointwise convergence.
+This is one of the key steps in the proof of the **Banach-Alaoglu** theorem. -/
+lemma is_closed_image_coe_closed_ball (f₀ : E →SL[σ₁₂] F) (r : ℝ) :
+  is_closed ((coe_fn : (E →SL[σ₁₂] F) → E → F) '' closed_ball f₀ r) :=
+is_closed_image_coe_of_bounded_of_weak_closed bounded_closed_ball (is_weak_closed_closed_ball f₀ r)
+
+/-- **Banach-Alaoglu** theorem. The set of functions `f : E → F` that represent continuous linear
+maps `f : E →SL[σ₁₂] F` at distance `≤ r` from `f₀ : E →SL[σ₁₂] F` is compact in the topology of
+pointwise convergence. Other versions of this theorem can be found in
+`analysis.normed_space.weak_dual`. -/
+lemma is_compact_image_coe_closed_ball [proper_space F] (f₀ : E →SL[σ₁₂] F) (r : ℝ) :
+  is_compact ((coe_fn : (E →SL[σ₁₂] F) → E → F) '' closed_ball f₀ r) :=
+is_compact_image_coe_of_bounded_of_weak_closed bounded_closed_ball $
+  is_weak_closed_closed_ball f₀ r
+
 end completeness
 
 section uniformly_extend

src/analysis/normed_space/weak_dual.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Kalle Kytölä. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kalle Kytölä
+Authors: Kalle Kytölä, Yury Kudryashov
 -/
 import topology.algebra.module.weak_dual
 import analysis.normed_space.dual
@@ -19,7 +19,9 @@ It is shown that the canonical mapping `normed_space.dual 𝕜 E → weak_dual 
 as a consequence the weak-* topology is coarser than the topology obtained from the operator norm
 (dual norm).
 
-The file is a stub, some TODOs below.
+In this file, we also establish the Banach-Alaoglu theorem about the compactness of closed balls
+in the dual of `E` (as well as sets of somewhat more general form) with respect to the weak-*
+topology.
 
 ## Main definitions
 
@@ -37,15 +39,21 @@ The first main result concerns the comparison of the operator norm topology on `
 weak-* topology on (its type synonym) `weak_dual 𝕜 E`:
 * `dual_norm_topology_le_weak_dual_topology`: The weak-* topology on the dual of a normed space is
   coarser (not necessarily strictly) than the operator norm topology.
+* `weak_dual.is_compact_polar` (a version of the Banach-Alaoglu theorem): The polar set of a
+  neighborhood of the origin in a normed space `E` over `𝕜` is compact in `weak_dual _ E`, if the
+  nondiscrete normed field `𝕜` is proper as a topological space.
+* `weak_dual.is_compact_closed_ball` (the most common special case of the Banach-Alaoglu theorem):
+  Closed balls in the dual of a normed space `E` over `ℝ` or `ℂ` are compact in the weak-star
+  topology.
 
 TODOs:
 * Add that in finite dimensions, the weak-* topology and the dual norm topology coincide.
 * Add that in infinite dimensions, the weak-* topology is strictly coarser than the dual norm
   topology.
-* Add Banach-Alaoglu theorem (general version maybe in `topology.algebra.module.weak_dual`).
-* Add metrizability of the dual unit ball (more generally bounded subsets) of `weak_dual 𝕜 E`
-  under the assumption of separability of `E`. Sequential Banach-Alaoglu theorem would then follow
-  from the general one.
+* Add metrizability of the dual unit ball (more generally weak-star compact subsets) of
+  `weak_dual 𝕜 E` under the assumption of separability of `E`.
+* Add the sequential Banach-Alaoglu theorem: the dual unit ball of a separable normed space `E`
+  is sequentially compact in the weak-star topology. This would follow from the metrizability above.
 
 ## Notations
 
@@ -58,9 +66,18 @@ Weak-* topology is defined generally in the file `topology.algebra.module.weak_d
 When `E` is a normed space, the duals `dual 𝕜 E` and `weak_dual 𝕜 E` are type synonyms with
 different topology instances.
 
+For the proof of Banach-Alaoglu theorem, the weak dual of `E` is embedded in the space of
+functions `E → 𝕜` with the topology of pointwise convergence.
+
+The polar set `polar 𝕜 s` of a subset `s` of `E` is originally defined as a subset of the dual
+`dual 𝕜 E`. We care about properties of these w.r.t. weak-* topology, and for this purpose give
+the definition `weak_dual.polar 𝕜 s` for the "same" subset viewed as a subset of `weak_dual 𝕜 E`
+(a type synonym of the dual but with a different topology instance).
+
 ## References
 
 * https://en.wikipedia.org/wiki/Weak_topology#Weak-*_topology
+* https://en.wikipedia.org/wiki/Banach%E2%80%93Alaoglu_theorem
 
 ## Tags
 
@@ -69,53 +86,37 @@ weak-star, weak dual
 -/
 
 noncomputable theory
-open filter
-open_locale topological_space
+open filter function metric set
+open_locale topological_space filter
 
 /-!
 ### Weak star topology on duals of normed spaces
+
 In this section, we prove properties about the weak-* topology on duals of normed spaces.
 We prove in particular that the canonical mapping `dual 𝕜 E → weak_dual 𝕜 E` is continuous,
 i.e., that the weak-* topology is coarser (not necessarily strictly) than the topology given
 by the dual-norm (i.e. the operator-norm).
 -/
 
-open normed_space
-
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 variables {E : Type*} [semi_normed_group E] [normed_space 𝕜 E]
 
-/-- For normed spaces `E`, there is a canonical map `dual 𝕜 E → weak_dual 𝕜 E` (the "identity"
-mapping). It is a linear equivalence. -/
-def normed_space.dual.to_weak_dual : dual 𝕜 E ≃ₗ[𝕜] weak_dual 𝕜 E :=
-linear_equiv.refl 𝕜 (E →L[𝕜] 𝕜)
+namespace normed_space
 
-/-- For normed spaces `E`, there is a canonical map `weak_dual 𝕜 E → dual 𝕜 E` (the "identity"
-mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
-equivalence `normed_space.dual.to_weak_dual` in the other direction. -/
-def weak_dual.to_normed_dual : weak_dual 𝕜 E ≃ₗ[𝕜] dual 𝕜 E :=
-normed_space.dual.to_weak_dual.symm
+namespace dual
 
-@[simp] lemma weak_dual.coe_to_fun_eq_normed_coe_to_fun (x' : dual 𝕜 E) :
-  (x'.to_weak_dual : E → 𝕜) = x' := rfl
+/-- For normed spaces `E`, there is a canonical map `dual 𝕜 E → weak_dual 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. -/
+def to_weak_dual : dual 𝕜 E ≃ₗ[𝕜] weak_dual 𝕜 E := linear_equiv.refl 𝕜 (E →L[𝕜] 𝕜)
 
-namespace normed_space.dual
+@[simp] lemma coe_to_weak_dual (x' : dual 𝕜 E) : ⇑(x'.to_weak_dual) = x' := rfl
 
 @[simp] lemma to_weak_dual_eq_iff (x' y' : dual 𝕜 E) :
   x'.to_weak_dual = y'.to_weak_dual ↔ x' = y' :=
 to_weak_dual.injective.eq_iff
 
-@[simp] lemma _root_.weak_dual.to_normed_dual_eq_iff (x' y' : weak_dual 𝕜 E) :
-  x'.to_normed_dual = y'.to_normed_dual ↔ x' = y' :=
-weak_dual.to_normed_dual.injective.eq_iff
-
-theorem to_weak_dual_continuous :
-  continuous (λ (x' : dual 𝕜 E), x'.to_weak_dual) :=
-begin
-  apply continuous_of_continuous_eval,
-  intros z,
-  exact (inclusion_in_double_dual 𝕜 E z).continuous,
-end
+theorem to_weak_dual_continuous : continuous (λ (x' : dual 𝕜 E), x'.to_weak_dual) :=
+continuous_of_continuous_eval _ $ λ z, (inclusion_in_double_dual 𝕜 E z).continuous
 
 /-- For a normed space `E`, according to `to_weak_dual_continuous` the "identity mapping"
 `dual 𝕜 E → weak_dual 𝕜 E` is continuous. This definition implements it as a continuous linear
@@ -127,25 +128,91 @@ def continuous_linear_map_to_weak_dual : dual 𝕜 E →L[𝕜] weak_dual 𝕜 E
 theorem dual_norm_topology_le_weak_dual_topology :
   (by apply_instance : topological_space (dual 𝕜 E)) ≤
     (by apply_instance : topological_space (weak_dual 𝕜 E)) :=
-begin
-  refine continuous.le_induced _,
-  apply continuous_pi_iff.mpr,
-  intros z,
-  exact (inclusion_in_double_dual 𝕜 E z).continuous,
-end
+by { convert to_weak_dual_continuous.le_induced, exact induced_id.symm }
 
-end normed_space.dual
+end dual
+end normed_space
 
 namespace weak_dual
 
-lemma to_normed_dual.preimage_closed_unit_ball :
-  (to_normed_dual ⁻¹' metric.closed_ball (0 : dual 𝕜 E) 1) =
-    {x' : weak_dual 𝕜 E | ∥ x'.to_normed_dual ∥ ≤ 1} :=
+open normed_space
+
+/-- For normed spaces `E`, there is a canonical map `weak_dual 𝕜 E → dual 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
+equivalence `normed_space.dual.to_weak_dual` in the other direction. -/
+def to_normed_dual : weak_dual 𝕜 E ≃ₗ[𝕜] dual 𝕜 E := normed_space.dual.to_weak_dual.symm
+
+@[simp] lemma coe_to_normed_dual (x' : weak_dual 𝕜 E) : ⇑(x'.to_normed_dual) = x' := rfl
+
+@[simp] lemma to_normed_dual_eq_iff (x' y' : weak_dual 𝕜 E) :
+  x'.to_normed_dual = y'.to_normed_dual ↔ x' = y' :=
+weak_dual.to_normed_dual.injective.eq_iff
+
+lemma is_closed_closed_ball (x' : dual 𝕜 E) (r : ℝ) :
+  is_closed (to_normed_dual ⁻¹' closed_ball x' r) :=
+is_closed_induced_iff'.2 (continuous_linear_map.is_weak_closed_closed_ball x' r)
+
+/-!
+### Polar sets in the weak dual space
+-/
+
+variables (𝕜)
+
+/-- The polar set `polar 𝕜 s` of `s : set E` seen as a subset of the dual of `E` with the
+weak-star topology is `weak_dual.polar 𝕜 s`. -/
+def polar (s : set E) : set (weak_dual 𝕜 E) := to_normed_dual ⁻¹' polar 𝕜 s
+
+lemma polar_def (s : set E) : polar 𝕜 s = {f : weak_dual 𝕜 E | ∀ x ∈ s, ∥f x∥ ≤ 1} := rfl
+
+/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
+is used. -/
+lemma is_closed_polar (s : set E) : is_closed (polar 𝕜 s) :=
 begin
-  have eq : metric.closed_ball (0 : dual 𝕜 E) 1 = {x' : dual 𝕜 E | ∥ x' ∥ ≤ 1},
-  { ext x', simp only [dist_zero_right, metric.mem_closed_ball, set.mem_set_of_eq], },
-  rw eq,
-  exact set.preimage_set_of_eq,
+  simp only [polar_def, set_of_forall],
+  exact is_closed_bInter (λ x hx, is_closed_Iic.preimage (eval_continuous _ _).norm)
 end
 
+variable {𝕜}
+
+/-- While the coercion `coe_fn : weak_dual 𝕜 E → (E → 𝕜)` is not a closed map, it sends *bounded*
+closed sets to closed sets. -/
+lemma is_closed_image_coe_of_bounded_of_closed {s : set (weak_dual 𝕜 E)}
+  (hb : bounded (dual.to_weak_dual ⁻¹' s)) (hc : is_closed s) :
+  is_closed ((coe_fn : weak_dual 𝕜 E → E → 𝕜) '' s) :=
+continuous_linear_map.is_closed_image_coe_of_bounded_of_weak_closed hb (is_closed_induced_iff'.1 hc)
+
+lemma is_compact_of_bounded_of_closed [proper_space 𝕜] {s : set (weak_dual 𝕜 E)}
+  (hb : bounded (dual.to_weak_dual ⁻¹' s)) (hc : is_closed s) :
+  is_compact s :=
+(embedding.is_compact_iff_is_compact_image fun_like.coe_injective.embedding_induced).mpr $
+  continuous_linear_map.is_compact_image_coe_of_bounded_of_closed_image hb $
+  is_closed_image_coe_of_bounded_of_closed hb hc
+
+variable (𝕜)
+
+/-- The image under `coe_fn : weak_dual 𝕜 E → (E → 𝕜)` of a polar `weak_dual.polar 𝕜 s` of a
+neighborhood `s` of the origin is a closed set. -/
+lemma is_closed_image_polar_of_mem_nhds {s : set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
+  is_closed ((coe_fn : weak_dual 𝕜 E → E → 𝕜) '' polar 𝕜 s) :=
+is_closed_image_coe_of_bounded_of_closed (bounded_polar_of_mem_nhds_zero 𝕜 s_nhd)
+  (is_closed_polar _ _)
+
+/-- The image under `coe_fn : normed_space.dual 𝕜 E → (E → 𝕜)` of a polar `polar 𝕜 s` of a
+neighborhood `s` of the origin is a closed set. -/
+lemma _root_.normed_space.dual.is_closed_image_polar_of_mem_nhds {s : set E}
+  (s_nhd : s ∈ 𝓝 (0 : E)) : is_closed ((coe_fn : dual 𝕜 E → E → 𝕜) '' normed_space.polar 𝕜 s) :=
+is_closed_image_polar_of_mem_nhds 𝕜 s_nhd
+
+/-- The **Banach-Alaoglu theorem**: the polar set of a neighborhood `s` of the origin in a
+normed space `E` is a compact subset of `weak_dual 𝕜 E`. -/
+theorem is_compact_polar [proper_space 𝕜] {s : set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
+  is_compact (polar 𝕜 s) :=
+is_compact_of_bounded_of_closed (bounded_polar_of_mem_nhds_zero 𝕜 s_nhd) (is_closed_polar _ _)
+
+/-- The **Banach-Alaoglu theorem**: closed balls of the dual of a normed space `E` are compact in
+the weak-star topology. -/
+theorem is_compact_closed_ball [proper_space 𝕜] (x' : dual 𝕜 E) (r : ℝ) :
+  is_compact (to_normed_dual ⁻¹' (closed_ball x' r)) :=
+is_compact_of_bounded_of_closed bounded_closed_ball (is_closed_closed_ball x' r)
+
 end weak_dual

src/topology/algebra/module/weak_dual.lean

@@ -180,9 +180,13 @@ weak_bilin (top_dual_pairing 𝕜 E)
 
 instance : inhabited (weak_dual 𝕜 E) := continuous_linear_map.inhabited
 
-instance add_monoid_hom_class_weak_dual : add_monoid_hom_class (weak_dual 𝕜 E) E 𝕜 :=
+instance weak_dual.add_monoid_hom_class : add_monoid_hom_class (weak_dual 𝕜 E) E 𝕜 :=
 continuous_linear_map.add_monoid_hom_class
 
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+instance : has_coe_to_fun (weak_dual 𝕜 E) (λ _, E → 𝕜) := fun_like.has_coe_to_fun
+
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `weak_dual 𝕜 E`. -/
 instance (M) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜]

src/topology/maps.lean

@@ -121,6 +121,10 @@ lemma inducing.is_closed_iff {f : α → β} (hf : inducing f) {s : set α} :
   is_closed s ↔ ∃ t, is_closed t ∧ f ⁻¹' t = s :=
 by rw [hf.induced, is_closed_induced_iff]
 
+lemma inducing.is_closed_iff' {f : α → β} (hf : inducing f) {s : set α} :
+  is_closed s ↔ ∀ x, f x ∈ closure (f '' s) → x ∈ s :=
+by rw [hf.induced, is_closed_induced_iff']
+
 lemma inducing.is_open_iff {f : α → β} (hf : inducing f) {s : set α} :
   is_open s ↔ ∃ t, is_open t ∧ f ⁻¹' t = s :=
 by rw [hf.induced, is_open_induced_iff]