[Merged by Bors] - feat(analysis/locally_convex): locally convex hausdorff spaces

src/analysis/locally_convex/with_seminorms.lean

@@ -289,6 +289,78 @@ begin
   rw (congr_fun (congr_arg (@nhds E) hp.1) 0),
   exact add_group_filter_basis.nhds_zero_has_basis _,
 end
+
+/-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
+are exactly the sets which contain seminorm balls around `x`.-/
+lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E) :
+  U ∈ nhds x ↔ ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
+begin
+  rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
+  split,
+  { rintros ⟨V, V_basis, hVU⟩,
+    rcases p.basis_sets_iff.mp V_basis with ⟨_, _, r_pos, V_ball⟩,
+    simp_rw [V_ball, seminorm.singleton_add_ball _, add_zero] at hVU,
+    exact ⟨_, _, r_pos, hVU⟩ },
+  { rintros ⟨s, r, r_pos, V_sub_U⟩,
+    refine ⟨(s.sup p).ball 0 r, p.basis_sets_iff.mpr ⟨_, _, r_pos, rfl⟩, _⟩,
+    simp_rw [seminorm.singleton_add_ball _, add_zero],
+    exact V_sub_U }
+end
+
+/-- The open sets of a space whose topology is induced by a family of seminorms
+are exactly the sets which contain seminorm balls around all of their points.-/
+lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E) :
+  is_open U ↔ ∀ (x ∈ U), ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
+by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
+
+/-- A separating family of seminorms induces a T₂ topology. -/
+lemma with_seminorms.t2_of_separating (hp : with_seminorms p) (h : ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) :
+  t2_space E :=
+begin
+  rw t2_space_iff_nhds,
+  intros x y hxy,
+  cases h (x - y) (sub_ne_zero.mpr hxy) with i pi_nonzero,
+  let r := p i (x - y),
+  have r_div_2_pos : p i (x - y) / 2 > 0 := by positivity,
+  have mem_nhds : ∀ x, (p i).ball x (r/2) ∈ nhds x :=
+  λ x, (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, r_div_2_pos, by rw finset.sup_singleton⟩,
+  use [(p i).ball x (r/2) , mem_nhds x, (p i).ball y (r/2), mem_nhds y],
+  intros W W_sub_xball W_sub_yball,
+  by_contra W_nonemp,
+  rw [le_bot_iff, bot_eq_empty, ←ne.def, ←nonempty_iff_ne_empty] at W_nonemp,
+  cases W_nonemp with z z_in_W,
+  have : r < r,
+  { calc
+    r   = p i (x - y)               : rfl
+    ... = p i ((x - z) + (z - y))   : by rw ←sub_add_sub_cancel
+    ... ≤ p i (x - z) + p i (z - y) : seminorm.add_le' _ _ _
+    ... = p i (z - x) + p i (z - y) : by rw [←map_neg_eq_map, neg_sub]
+    ... < r/2 + r/2                 : add_lt_add (W_sub_xball z_in_W) (W_sub_yball z_in_W)
+    ... = r                         : add_halves _ },
+  rwa lt_self_iff_false r at this
+end
+
+/-- A family of seminorms inducing a T₂ topology is separating. -/
+lemma with_seminorms.separating_of_t2 [t2_space E] (hp : with_seminorms p) (x : E) (hx : x ≠ 0) :
+  ∃ i, p i x ≠ 0 :=
+begin
+  rcases t2_separation hx with ⟨U, V, hU, hV, hxU, h0V, UV_disj⟩,
+  rcases (with_seminorms.is_open_iff_mem_balls hp _).mp hV 0 h0V with ⟨s, r, r_pos, ball_V⟩,
+  have hpx_nezero : (s.sup p) x ≠ 0,
+  { intro hsup_px,
+    refine (set.singleton_nonempty x).not_subset_empty (UV_disj _ _);
+      rw [set.le_eq_subset, set.singleton_subset_iff],
+    { exact hxU },
+    { refine ball_V _,
+      rwa [seminorm.mem_ball, sub_zero, hsup_px] } },
+  rw seminorm.finset_sup_apply at hpx_nezero,
+  have := hpx_nezero.symm.lt_of_le,
+  simp only [nnreal.zero_le_coe, nnreal.coe_pos,
+    finset.lt_sup_iff, exists_prop, forall_true_left] at this,
+  rcases this with ⟨i, his, hpix_pos⟩,
+  use ⟨i, ne_of_gt hpix_pos⟩
+end
+
 end topology
 
 section topological_add_group

src/analysis/seminorm.lean

@@ -609,6 +609,24 @@ begin
   exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)
 end
 
+lemma sub_mem_ball (p : seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
+  x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r :=
+by simp_rw [mem_ball, sub_sub]
+
+/- Can this be done more neatly with `seminorm.ball_comp`?
+Alternatively, can this be done using/imitating the ball-addition-lemmas
+in `normed_space/pointwise`? -/
+/-- The image of a ball under addition with a singleton is another ball. -/
+lemma singleton_add_ball (p : seminorm 𝕜 E) :
+  (λ (z : E), x + z) '' p.ball y r = p.ball (x + y) r :=
+begin
+  apply le_antisymm,
+  { rintros _ ⟨_, _, hz₁z₀⟩,
+    rwa [mem_ball, ←hz₁z₀, add_sub_add_left_eq_sub] },
+  { exact λ z hz, ⟨z - x, ⟨(p.sub_mem_ball _ _ _ _).mpr hz, add_eq_of_eq_sub' rfl⟩⟩ }
+
+end
+
 end has_smul
 
 section module