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

src/analysis/locally_convex/with_seminorms.lean

@@ -289,6 +289,82 @@ 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 ↔ ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+begin
+  rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
+  split,
+  { rintros ⟨V, V_in_basis, V_sub_U⟩,
+    rcases p.basis_sets_iff.mp V_in_basis with ⟨i_set, ε, ε_pos, hr⟩,
+    simp_rw [hr, seminorm.singleton_add_ball _, add_zero] at V_sub_U,
+    exact ⟨_, _, ε_pos, V_sub_U⟩ },
+  { rintros ⟨i_set, ε, ε_pos, V_sub_U⟩,
+    refine ⟨(i_set.sup p).ball 0 ε, p.basis_sets_iff.mpr ⟨_, _, ε_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), ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
+
+/-- A space whose topology is induced by a family of seminorms is Hausdorff iff
+the family of seminorms is separating. -/
+theorem with_seminorms.t2_iff_separating (hp : with_seminorms p) :
+  t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
+begin
+  split,
+  { introI t2,
+    intros x x_ne_zero,
+    rcases t2_separation x_ne_zero with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
+    rcases (with_seminorms.is_open_iff_mem_balls hp _).mp v_open 0 zero_in_v
+      with ⟨i_set, ε, ε_pos, ball_in_v⟩,
+    have sup_p_x_ne_zero : (i_set.sup p) x ≠ 0,
+    { intro assump,
+      refine (set.singleton_nonempty x).not_subset_empty (u_v_disj _ _);
+        rw [set.le_eq_subset, set.singleton_subset_iff],
+      { exact (x_in_u) },
+      { refine (ball_in_v _),
+        rwa [seminorm.mem_ball, sub_zero, assump] } },
+    rw seminorm.finset_sup_apply at sup_p_x_ne_zero,
+    have := (ne.symm sup_p_x_ne_zero).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, i_in_set, p_i_pos⟩,
+    use ⟨i, ne_of_gt p_i_pos⟩ },
+  { rw t2_iff_nhds,
+    intros h x y x_y_nhds_ne_bot,
+    rw filter.inf_ne_bot_iff at x_y_nhds_ne_bot,
+    by_contra x_neq_y,
+    cases h (x - y) (sub_ne_zero.mpr x_neq_y) with i pi_nonzero,
+    let ε := (p i) (x - y),
+    let sx := (p i).ball x (ε/2),
+    let sy := (p i).ball y (ε/2),
+    have ε_div_2_pos := div_pos ((ne.symm pi_nonzero).lt_of_le (map_nonneg _ _)) zero_lt_two,
+    have sx_nhds_x : sx ∈ nhds x :=
+      (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, ε_div_2_pos, by rw finset.sup_singleton⟩,
+    have sy_nhds_y : sy ∈ nhds y :=
+      (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, ε_div_2_pos, by rw finset.sup_singleton⟩,
+    cases set.nonempty_def.mp (x_y_nhds_ne_bot sx_nhds_x sy_nhds_y) with z z_in_inter,
+    obtain ⟨lt1, lt2⟩ := (set.mem_inter_iff _ _ _).mp z_in_inter,
+    rw seminorm.mem_ball at lt1 lt2,
+    have : ε < ε,
+    { calc
+      ε   = 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]
+      ... < ε/2 + ε/2                  : add_lt_add lt1 lt2
+      ... = ε                          : add_halves _ },
+    rwa lt_self_iff_false ε at this }
+end
+
+
 end topology
 
 section topological_add_group

src/analysis/seminorm.lean

@@ -609,6 +609,22 @@ begin
   exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)
 end
 
+/- 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 w ⟨w', w'_in_ball, w'h⟩,
+    rwa [mem_ball, ← w'h, add_sub_add_left_eq_sub] },
+  { intros w w_in_ball,
+    refine set.mem_image_iff_bex.mpr ⟨w - x , _⟩,
+    rw [mem_ball, sub_sub, add_sub, add_sub_cancel'],
+    exact ⟨w_in_ball, rfl⟩ }
+end
+
 end has_smul
 
 section module