feat(analysis/normed_space/finite_dimension): a finite dimensional af…

…fine subspace is closed (#13440)

src/analysis/normed_space/add_torsor.lean

@@ -6,6 +6,7 @@ Authors: Joseph Myers, Yury Kudryashov
 import analysis.normed_space.basic
 import analysis.normed.group.add_torsor
 import linear_algebra.affine_space.midpoint
+import linear_algebra.affine_space.affine_subspace
 import topology.instances.real_vector_space
 
 /-!
@@ -21,14 +22,23 @@ open filter
 variables {α V P : Type*} [semi_normed_group V] [pseudo_metric_space P] [normed_add_torsor V P]
 variables {W Q : Type*} [normed_group W] [metric_space Q] [normed_add_torsor W Q]
 
-include V
-
 section normed_space
 
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V]
 
 open affine_map
 
+lemma affine_subspace.is_closed_direction_iff [normed_space 𝕜 W] (s : affine_subspace 𝕜 Q) :
+  is_closed (s.direction : set W) ↔ is_closed (s : set Q) :=
+begin
+  rcases s.eq_bot_or_nonempty with rfl|⟨x, hx⟩, { simp [is_closed_singleton] },
+  rw [← (isometric.vadd_const x).to_homeomorph.symm.is_closed_image,
+    affine_subspace.coe_direction_eq_vsub_set_right hx],
+  refl
+end
+
+include V
+
 @[simp] lemma dist_center_homothety (p₁ p₂ : P) (c : 𝕜) :
   dist p₁ (homothety p₁ c p₂) = ∥c∥ * dist p₁ p₂ :=
 by simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]
@@ -118,7 +128,7 @@ lemma dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
   dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 :=
 by simpa using dist_midpoint_midpoint_le' p₁ p₂ p₃ p₄
 
-include W
+include V W
 
 /-- A continuous map between two normed affine spaces is an affine map provided that
 it sends midpoints to midpoints. -/

src/analysis/normed_space/finite_dimension.lean

@@ -238,11 +238,37 @@ begin
   rw [basis.equiv_fun_symm_apply, basis.sum_repr]
 end
 
-theorem affine_map.continuous_of_finite_dimensional {PE PF : Type*}
-  [metric_space PE] [normed_add_torsor E PE] [metric_space PF] [normed_add_torsor F PF]
-  [finite_dimensional 𝕜 E] (f : PE →ᵃ[𝕜] PF) : continuous f :=
+section affine
+
+variables  {PE PF : Type*} [metric_space PE] [normed_add_torsor E PE] [metric_space PF]
+  [normed_add_torsor F PF] [finite_dimensional 𝕜 E]
+
+include E F
+
+theorem affine_map.continuous_of_finite_dimensional (f : PE →ᵃ[𝕜] PF) : continuous f :=
 affine_map.continuous_linear_iff.1 f.linear.continuous_of_finite_dimensional
 
+theorem affine_equiv.continuous_of_finite_dimensional (f : PE ≃ᵃ[𝕜] PF) : continuous f :=
+f.to_affine_map.continuous_of_finite_dimensional
+
+/-- Reinterpret an affine equivalence as a homeomorphism. -/
+def affine_equiv.to_homeomorph_of_finite_dimensional (f : PE ≃ᵃ[𝕜] PF) : PE ≃ₜ PF :=
+{ to_equiv := f.to_equiv,
+  continuous_to_fun := f.continuous_of_finite_dimensional,
+  continuous_inv_fun :=
+    begin
+      haveI : finite_dimensional 𝕜 F, from f.linear.finite_dimensional,
+      exact f.symm.continuous_of_finite_dimensional
+    end }
+
+@[simp] lemma affine_equiv.coe_to_homeomorph_of_finite_dimensional (f : PE ≃ᵃ[𝕜] PF) :
+  ⇑f.to_homeomorph_of_finite_dimensional = f := rfl
+
+@[simp] lemma affine_equiv.coe_to_homeomorph_of_finite_dimensional_symm (f : PE ≃ᵃ[𝕜] PF) :
+  ⇑f.to_homeomorph_of_finite_dimensional.symm = f.symm := rfl
+
+end affine
+
 lemma continuous_linear_map.continuous_det :
   continuous (λ (f : E →L[𝕜] E), f.det) :=
 begin
@@ -593,6 +619,11 @@ lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dime
   is_closed (s : set E) :=
 s.complete_of_finite_dimensional.is_closed
 
+lemma affine_subspace.closed_of_finite_dimensional {P : Type*} [metric_space P]
+  [normed_add_torsor E P] (s : affine_subspace 𝕜 P) [finite_dimensional 𝕜 s.direction] :
+  is_closed (s : set P) :=
+s.is_closed_direction_iff.mp s.direction.closed_of_finite_dimensional
+
 section riesz
 
 /-- In an infinite dimensional space, given a finite number of points, one may find a point