feat(analysis/metric_space): sup metric for product of metric spaces

Author: digama0

algebra/linear_algebra/multivariate_polynomial.lean

@@ -108,13 +108,13 @@ instance : has_add (mv_polynomial σ α) := finsupp.has_add
 instance : has_mul (mv_polynomial σ α) := finsupp.has_mul
 instance : comm_semiring (mv_polynomial σ α) := finsupp.to_comm_semiring
 
-/-- monomial s a is the monomial `a * X^s` -/
+/-- `monomial s a` is the monomial `a * X^s` -/
 def monomial (s : σ →₀ ℕ) (a : α) : mv_polynomial σ α := single s a
 
-/-- C a is the constant polynomial with value a -/
+/-- `C a` is the constant polynomial with value `a` -/
 def C (a : α) : mv_polynomial σ α := monomial 0 a
 
-/-- X n is the polynomial with value X_n -/
+/-- `X n` is the polynomial with value X_n -/
 def X (n : σ) : mv_polynomial σ α := monomial (single n 1) 1
 
 @[simp] lemma C_0 : C 0 = (0 : mv_polynomial σ α) := by simp [C, monomial]; refl

analysis/metric_space.lean

@@ -99,6 +99,9 @@ nonneg_of_mul_nonneg_left this two_pos
 theorem dist_pos_of_ne {x y : α} (h : x ≠ y) : dist x y > 0 :=
 lt_of_le_of_ne dist_nonneg (by simp * at *)
 
+theorem dist_le_zero_iff {x y : α} : dist x y ≤ 0 ↔ x = y :=
+by simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero_iff _ _ x y
+
 theorem ne_of_dist_pos {x y : α} (h : dist x y > 0) : x ≠ y :=
 assume : x = y,
 have 0 < (0:real), by simp [this] at h; exact h,
@@ -239,3 +242,23 @@ end
 
 theorem is_open_metric : is_open s ↔ (∀x∈s, ∃ε>0, open_ball x ε ⊆ s) :=
 by simp [is_open_iff_nhds, mem_nhds_sets_iff_metric]
+
+instance prod.metric_space_max [metric_space α] [metric_space β] : metric_space (α × β) :=
+{ dist := λ x y, max (dist x.1 y.1) (dist x.2 y.2),
+  dist_self := λ x, by simp,
+  eq_of_dist_eq_zero := λ x y h, begin
+    cases max_le_iff.1 (le_of_eq h) with h₁ h₂,
+    exact prod.ext.2 ⟨dist_le_zero_iff.1 h₁, dist_le_zero_iff.1 h₂⟩
+  end,
+  dist_comm := λ x y, by simp [dist_comm],
+  dist_triangle := λ x y z, max_le
+    (le_trans (dist_triangle _ _ _) (add_le_add (le_max_left _ _) (le_max_left _ _)))
+    (le_trans (dist_triangle _ _ _) (add_le_add (le_max_right _ _) (le_max_right _ _))),
+  uniformity_dist := begin
+    refine prod_uniformity.trans _,
+    simp [uniformity_dist, vmap_infi],
+    rw ← infi_inf_eq, congr, funext,
+    rw ← infi_inf_eq, congr, funext,
+    simp [inf_principal, set_eq_def, max_lt_iff]
+  end,
+  to_uniform_space := prod.uniform_space }

analysis/topology/topological_space.lean

@@ -419,7 +419,7 @@ end locally_finite
 /- compact sets -/
 section compact
 
-/-- A set `s` is compact if every filter that contains `s` also contains every
+/-- A set `s` is compact if every filter that contains `s` also meets every
   neighborhood of some `a ∈ s`. -/
 def compact (s : set α) := ∀f, f ≠ ⊥ → f ≤ principal s → ∃a∈s, f ⊓ nhds a ≠ ⊥
 
@@ -654,6 +654,7 @@ end topological_space
 namespace topological_space
 variables {α : Type u}
 
+/-- The least topology containing a collection of basic sets. -/
 inductive generate_open (g : set (set α)) : set α → Prop
 | basic  : ∀s∈g, generate_open s
 | univ   : generate_open univ
@@ -742,7 +743,7 @@ lemma is_closed_induced_iff [t : topological_space β] {s : set α} {f : α →
   assume ⟨t, ht, heq⟩, ⟨-t, ht, by simp [preimage_compl, heq.symm]⟩⟩
 
 /-- Given `f : α → β` and a topology on `α`, the coinduced topology on `β` is defined
-  such that `s:set β` is open if the preimage of `s` is open. This is the coarsest topology that
+  such that `s:set β` is open if the preimage of `s` is open. This is the finest topology that
   makes `f` continuous. -/
 def topological_space.coinduced {α : Type u} {β : Type v} (f : α → β) (t : topological_space α) :
   topological_space β :=

analysis/topology/uniform_space.lean

@@ -1382,6 +1382,11 @@ uniform_space.of_core_eq
       by rw [to_topological_space_sup, to_topological_space_vmap, to_topological_space_vmap]; refl
     ... = _ : by rw [uniform_space.to_core_to_topological_space])
 
+theorem prod_uniformity [uniform_space α] [uniform_space β] : @uniformity (α × β) _ =
+  uniformity.vmap (λp:(α × β) × α × β, (p.1.1, p.2.1)) ⊓
+  uniformity.vmap (λp:(α × β) × α × β, (p.1.2, p.2.2)) :=
+sup_uniformity
+
 lemma uniform_embedding_subtype_emb {α : Type*} {β : Type*} [uniform_space α] [uniform_space β]
   (p : α → Prop) {e : α → β} (ue : uniform_embedding e) (de : dense_embedding e) :
   uniform_embedding (de.subtype_emb p) :=

data/equiv.lean

@@ -312,7 +312,7 @@ section
 def arrow_prod_equiv_prod_arrow (α β γ : Type*) : (γ → α × β) ≃ ((γ → α) × (γ → β)) :=
 ⟨λ f, (λ c, (f c).1, λ c, (f c).2),
  λ p c, (p.1 c, p.2 c),
- λ f, funext $ λ c, prod.mk.eta,
+ λ f, funext $ λ c, prod.mk.eta _,
  λ p, by cases p; refl⟩
 
 def arrow_arrow_equiv_prod_arrow (α β γ : Sort*) : (α → β → γ) ≃ (α × β → γ) :=

data/prod.lean

@@ -18,12 +18,15 @@ variables {α : Type u} {β : Type v}
 namespace prod
 
 -- copied from parser
-@[simp] lemma mk.eta : ∀{p : α × β}, (p.1, p.2) = p
+@[simp] lemma mk.eta : ∀ p : α × β, (p.1, p.2) = p
 | (a, b) := rfl
 
 @[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=
 ⟨prod.mk.inj, by cc⟩
 
+lemma ext {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 :=
+by rw [← mk.eta p, ← mk.eta q, mk.inj_iff]
+
 /-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
 def swap : α × β → β × α := λp, (p.2, p.1)
 

order/complete_lattice.lean

@@ -346,7 +346,7 @@ le_antisymm
 
 attribute [ematch] le_refl
 
-theorem infi_inf_eq {f g : β → α} : (⨅ x, f x ⊓ g x) = (⨅ x, f x) ⊓ (⨅ x, g x) :=
+theorem infi_inf_eq {f g : ι → α} : (⨅ x, f x ⊓ g x) = (⨅ x, f x) ⊓ (⨅ x, g x) :=
 le_antisymm
   (le_inf
     (le_infi $ assume i, infi_le_of_le i inf_le_left)