feat(analysis/normed_space/lattice_ordered_group): prove `order_close…

…d_topology` for `normed_lattice_add_comm_group` (#10838)

src/analysis/normed_space/lattice_ordered_group.lean

@@ -162,3 +162,45 @@ topological_lattice.mk
 lemma norm_abs_sub_abs (a b : α) :
   ∥ |a| - |b| ∥ ≤ ∥a-b∥ :=
 solid (lattice_ordered_comm_group.abs_abs_sub_abs_le _ _)
+
+lemma norm_sup_sub_sup_le_norm (x y z : α) : ∥x ⊔ z - (y ⊔ z)∥ ≤ ∥x - y∥ :=
+solid (abs_sup_sub_sup_le_abs x y z)
+
+lemma norm_inf_sub_inf_le_norm (x y z : α) : ∥x ⊓ z - (y ⊓ z)∥ ≤ ∥x - y∥ :=
+solid (abs_inf_sub_inf_le_abs x y z)
+
+lemma lipschitz_with_sup_right (z : α) : lipschitz_with 1 (λ x, x ⊔ z) :=
+lipschitz_with.of_dist_le_mul $ λ x y, by
+{ rw [nonneg.coe_one, one_mul, dist_eq_norm, dist_eq_norm], exact norm_sup_sub_sup_le_norm x y z, }
+
+lemma lipschitz_with_pos : lipschitz_with 1 (has_pos_part.pos : α → α) :=
+lipschitz_with_sup_right 0
+
+lemma continuous_pos : continuous (has_pos_part.pos : α → α) :=
+lipschitz_with.continuous lipschitz_with_pos
+
+lemma continuous_neg' : continuous (has_neg_part.neg : α → α) :=
+continuous_pos.comp continuous_neg
+
+lemma is_closed_nonneg {E} [normed_lattice_add_comm_group E] : is_closed {x : E | 0 ≤ x} :=
+begin
+  suffices : {x : E | 0 ≤ x} = has_neg_part.neg ⁻¹' {(0 : E)},
+  by { rw this, exact is_closed.preimage continuous_neg' is_closed_singleton, },
+  ext1 x,
+  simp only [set.mem_preimage, set.mem_singleton_iff, set.mem_set_of_eq, neg_eq_zero_iff],
+end
+
+lemma is_closed_le_of_is_closed_nonneg {G} [ordered_add_comm_group G] [topological_space G]
+  [has_continuous_sub G] (h : is_closed {x : G | 0 ≤ x}) :
+  is_closed {p : G × G | p.fst ≤ p.snd} :=
+begin
+  have : {p : G × G | p.fst ≤ p.snd} = (λ p : G × G, p.snd - p.fst) ⁻¹' {x : G | 0 ≤ x},
+    by { ext1 p, simp only [sub_nonneg, set.preimage_set_of_eq], },
+  rw this,
+  exact is_closed.preimage (continuous_snd.sub continuous_fst) h,
+end
+
+@[priority 100]  -- See note [lower instance priority]
+instance normed_lattice_add_comm_group.order_closed_topology {E} [normed_lattice_add_comm_group E] :
+  order_closed_topology E :=
+⟨is_closed_le_of_is_closed_nonneg is_closed_nonneg⟩