From 91c0ef86c522355b76acbfa92def7e9512144e72 Mon Sep 17 00:00:00 2001 From: kkytola Date: Wed, 4 May 2022 20:04:15 +0000 Subject: [PATCH] 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 Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com> --- src/analysis/normed_space/dual.lean | 4 +- src/analysis/normed_space/operator_norm.lean | 76 ++++++++- src/analysis/normed_space/weak_dual.lean | 161 +++++++++++++------ src/topology/algebra/module/weak_dual.lean | 6 +- src/topology/maps.lean | 4 + src/topology/order.lean | 7 +- 6 files changed, 205 insertions(+), 53 deletions(-) diff --git a/src/analysis/normed_space/dual.lean b/src/analysis/normed_space/dual.lean index b9987efac9c29..7127fe14ad1ce 100644 --- a/src/analysis/normed_space/dual.lean +++ b/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 diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean index e0090f6bfa77f..487928749e3cc 100644 --- a/src/analysis/normed_space/operator_norm.lean +++ b/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 diff --git a/src/analysis/normed_space/weak_dual.lean b/src/analysis/normed_space/weak_dual.lean index 4bac47c508a80..f405d40bf1078 100644 --- a/src/analysis/normed_space/weak_dual.lean +++ b/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 diff --git a/src/topology/algebra/module/weak_dual.lean b/src/topology/algebra/module/weak_dual.lean index 8adef9c5d0840..10c9126b6706f 100644 --- a/src/topology/algebra/module/weak_dual.lean +++ b/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 π•œ] diff --git a/src/topology/maps.lean b/src/topology/maps.lean index 7cd38018c8dd1..3dcbb381db248 100644 --- a/src/topology/maps.lean +++ b/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] diff --git a/src/topology/order.lean b/src/topology/order.lean index ede00f242234c..8ceb8536a921a 100644 --- a/src/topology/order.lean +++ b/src/topology/order.lean @@ -330,8 +330,7 @@ lemma is_closed_induced_iff [t : topological_space Ξ²] {s : set Ξ±} {f : Ξ± β†’ @is_closed Ξ± (t.induced f) s ↔ (βˆƒt, is_closed t ∧ f ⁻¹' t = s) := begin simp only [← is_open_compl_iff, is_open_induced_iff], - exact ⟨λ ⟨t, ht, heq⟩, ⟨tᢜ, by rwa compl_compl, by simp [preimage_compl, heq, compl_compl]⟩, - Ξ» ⟨t, ht, heq⟩, ⟨tᢜ, ht, by simp only [preimage_compl, heq.symm]⟩⟩ + exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff]) end /-- Given `f : Ξ± β†’ Ξ²` and a topology on `Ξ±`, the coinduced topology on `Ξ²` is defined @@ -780,6 +779,10 @@ lemma closure_induced [t : topological_space Ξ²] {f : Ξ± β†’ Ξ²} {a : Ξ±} {s : s a ∈ @closure Ξ± (topological_space.induced f t) s ↔ f a ∈ closure (f '' s) := by simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm] +lemma is_closed_induced_iff' [t : topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} : + @is_closed Ξ± (t.induced f) s ↔ βˆ€ a, f a ∈ closure (f '' s) β†’ a ∈ s := +by simp only [← closure_subset_iff_is_closed, subset_def, closure_induced] + end induced section sierpinski