From d1cbb8f0c6d79928a652ee27804edbd598b208c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Sat, 26 Aug 2017 15:33:39 -0400 Subject: [PATCH 1/4] fix(algebra/group): add every transport theorem from main Lean repository --- algebra/group.lean | 99 ++++++++++++++++++++++++++++++++++++++++------ topology/real.lean | 2 +- 2 files changed, 88 insertions(+), 13 deletions(-) diff --git a/algebra/group.lean b/algebra/group.lean index 0e048ed39bfdd..4664c65f97269 100644 --- a/algebra/group.lean +++ b/algebra/group.lean @@ -42,18 +42,93 @@ section group end group /- transport versions to additive -/ -run_cmd transport_multiplicative_to_additive - [ (`left_inverse_inv, `left_inverse_neg), - (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq), - (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero), - (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero), - (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg), - (`mul_right_inv, `add_right_inv), - (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero), - (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add), - (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg) - -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero) not needed for commutative groups - -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero) +run_cmd transport_multiplicative_to_additive [ + /- map operations -/ + (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg), + (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg), + /- map constructors -/ + (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk), + /- map structures -/ + (`semigroup, `add_semigroup), + (`monoid, `add_monoid), + (`group, `add_group), + (`comm_semigroup, `add_comm_semigroup), + (`comm_monoid, `add_comm_monoid), + (`comm_group, `add_comm_group), + (`left_cancel_semigroup, `add_left_cancel_semigroup), + (`right_cancel_semigroup, `add_right_cancel_semigroup), + (`left_cancel_semigroup.mk, `add_left_cancel_semigroup.mk), + (`right_cancel_semigroup.mk, `add_right_cancel_semigroup.mk), + /- map instances -/ + (`semigroup.to_has_mul, `add_semigroup.to_has_add), + (`monoid.to_has_one, `add_monoid.to_has_zero), + (`group.to_has_inv, `add_group.to_has_neg), + (`comm_semigroup.to_semigroup, `add_comm_semigroup.to_add_semigroup), + (`monoid.to_semigroup, `add_monoid.to_add_semigroup), + (`comm_monoid.to_monoid, `add_comm_monoid.to_add_monoid), + (`comm_monoid.to_comm_semigroup, `add_comm_monoid.to_add_comm_semigroup), + (`group.to_monoid, `add_group.to_add_monoid), + (`comm_group.to_group, `add_comm_group.to_add_group), + (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid), + (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup), + (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup), + /- map projections -/ + (`semigroup.mul_assoc, `add_semigroup.add_assoc), + (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm), + (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel), + (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel), + (`monoid.one_mul, `add_monoid.zero_add), + (`monoid.mul_one, `add_monoid.add_zero), + (`group.mul_left_inv, `add_group.add_left_neg), + (`group.mul, `add_group.add), + (`group.mul_assoc, `add_group.add_assoc), + /- map lemmas -/ + (`mul_assoc, `add_assoc), + (`mul_comm, `add_comm), + (`mul_left_comm, `add_left_comm), + (`mul_right_comm, `add_right_comm), + (`one_mul, `zero_add), + (`mul_one, `add_zero), + (`mul_left_inv, `add_left_neg), + (`mul_left_cancel, `add_left_cancel), + (`mul_right_cancel, `add_right_cancel), + (`mul_left_cancel_iff, `add_left_cancel_iff), + (`mul_right_cancel_iff, `add_right_cancel_iff), + (`inv_mul_cancel_left, `neg_add_cancel_left), + (`inv_mul_cancel_right, `neg_add_cancel_right), + (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq), + (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero), + (`inv_inv, `neg_neg), + (`mul_right_inv, `add_right_neg), + (`mul_inv_cancel_left, `add_neg_cancel_left), + (`mul_inv_cancel_right, `add_neg_cancel_right), + (`mul_inv_rev, `neg_add_rev), + (`mul_inv, `neg_add), + (`inv_inj, `neg_inj), + (`group.mul_left_cancel, `add_group.add_left_cancel), + (`group.mul_right_cancel, `add_group.add_right_cancel), + (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup), + (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup), + (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg), + (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero), + (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq), + (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add), + (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add), + (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq), + (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq), + (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add), + (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg), + (`one_inv, `neg_zero), + (`left_inverse_inv, `left_inverse_neg), + (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq), + (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero), + (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero), + (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg), + (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero), + (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add), + (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg) + -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero) not needed for commutative groups + -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero) ] section add_group diff --git a/topology/real.lean b/topology/real.lean index bf459fb53523f..2806843621584 100644 --- a/topology/real.lean +++ b/topology/real.lean @@ -1117,7 +1117,7 @@ instance : discrete_linear_ordered_field ℝ := decidable_le := by apply_instance, decidable_lt := by apply_instance } -instance : topological_ring ℝ := +instance : topological_ring ℝ := { real.topological_add_group with continuous_mul := continuous_mul_real } lemma compact_ivl {a b : ℝ} : compact {r:ℝ | a ≤ r ∧ r ≤ b } := From f1fba68d444538fd939e7221107d99c40349041b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Tue, 22 Aug 2017 10:02:25 -0400 Subject: [PATCH 2/4] feat(algebra): porting modules from lean2 --- algebra/module.lean | 67 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 algebra/module.lean diff --git a/algebra/module.lean b/algebra/module.lean new file mode 100644 index 0000000000000..77b1a5335dd01 --- /dev/null +++ b/algebra/module.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2015 Nathaniel Thomas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nathaniel Thomas, Jeremy Avigad + +Modules and vector spaces over a ring. +-/ +import algebra.field + +universes u v + +class has_scalar (α : inout Type u) (γ : Type v) := (smul : α → γ → γ) + +infixl ` • `:73 := has_scalar.smul + +/- modules over a ring -/ + +class module (α : inout Type u) (β : Type v) [ring α] extends has_scalar α β, add_comm_group β := +(smul_left_distrib : ∀r (x y : β), r • (x + y) = r • x + r • y) +(smul_right_distrib : ∀r s (x : β), (r + s) • x = r • x + s • x) +(mul_smul : ∀r s (x : β), (r * s) • x = r • (s • x)) +(one_smul : ∀x : β, (1 : α) • x = x) + +section module +variables {α : Type u} {β : Type v} [ring α] [module α β] +variables {a b c : α} {u v w : β} + +theorem smul_left_distrib : a • (u + v) = a • u + a • v := module.smul_left_distrib _ a u v +theorem smul_right_distrib : (a + b) • u = a • u + b • u := module.smul_right_distrib _ a b u +theorem mul_smul : (a * b) • u = a • (b • u) := module.mul_smul _ a b u +@[simp] theorem one_smul : (1 : α) • u = u := module.one_smul _ u + +@[simp] theorem zero_smul : (0 : α) • u = 0 := +have (0 : α) • u + 0 • u = 0 • u + 0, by rewrite [←smul_right_distrib]; simp, +add_left_cancel this + +@[simp] theorem smul_zero : a • (0 : β) = 0 := +have a • (0:β) + a • 0 = a • 0 + 0, by rewrite [←smul_left_distrib]; simp, +add_left_cancel this + +@[simp] theorem neg_smul : (-a) • u = - (a • u) := +eq_neg_of_add_eq_zero (by rewrite [←smul_right_distrib, add_left_neg, zero_smul]) + +@[simp] theorem smul_neg : a • (-u) = -(a • u) := +calc a • (-u) = a • (-(1 • u)) : by simp + ... = (a * -1) • u : by rw [←neg_smul, mul_smul]; simp + ... = -(a • u) : by rw [mul_neg_eq_neg_mul_symm]; simp + +theorem smul_sub_left_distrib (a : α) (u v : β) : a • (u - v) = a • u - a • v := +by simp [smul_left_distrib] + +theorem sub_smul_right_distrib (a b : α) (v : β) : (a - b) • v = a • v - b • v := +by simp [smul_right_distrib] + +end module + +def ring.to_module {α : Type u} [r : ring α] : module α α := +{ r with + smul := λa b, a * b, + smul_left_distrib := assume a b c, mul_add _ _ _, + smul_right_distrib := assume a b c, add_mul _ _ _, + mul_smul := assume a b c, mul_assoc _ _ _, + one_smul := assume a, one_mul _ } + +/- vector spaces -/ + +class vector_space (α : inout Type u) (β : Type v) [field α] extends module α β From 5b3b136accaa8cad6d32a006ee4aa171eb9a061c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Thu, 24 Aug 2017 14:53:29 -0400 Subject: [PATCH 3/4] feat(topology): port metric space from lean2 --- algebra/field.lean | 14 +++ algebra/group.lean | 3 + data/rat.lean | 2 +- order/basic.lean | 42 +++++++ order/complete_lattice.lean | 14 ++- order/filter.lean | 43 +++++-- topology/metric_space.lean | 219 ++++++++++++++++++++++++++++++++++++ topology/real.lean | 14 +-- topology/uniform_space.lean | 13 ++- 9 files changed, 339 insertions(+), 25 deletions(-) create mode 100644 topology/metric_space.lean diff --git a/algebra/field.lean b/algebra/field.lean index 468cb7bdcd6ff..526959d6400a3 100644 --- a/algebra/field.lean +++ b/algebra/field.lean @@ -50,6 +50,20 @@ calc (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x / c) ⁻¹' {r | a ≤ ... = {r | a * c ≤ r ∧ r ≤ b * c} : set.ext $ by simp [le_div_iff_mul_le_of_pos, div_le_iff_le_mul_of_pos, hc] +instance linear_ordered_field.to_densely_ordered [linear_ordered_field α] : densely_ordered α := +{ dense := assume a₁ a₂ h, ⟨(a₁ + a₂) / 2, + calc a₁ = (a₁ + a₁) / 2 : (add_self_div_two a₁).symm + ... < (a₁ + a₂) / 2 : div_lt_div_of_lt_of_pos (add_lt_add_left h _) two_pos, + calc (a₁ + a₂) / 2 < (a₂ + a₂) / 2 : div_lt_div_of_lt_of_pos (add_lt_add_right h _) two_pos + ... = a₂ : add_self_div_two a₂⟩ } + +instance linear_ordered_field.to_no_top_order [linear_ordered_field α] : no_top_order α := +{ no_top := assume a, ⟨a + 1, lt_add_of_le_of_pos (le_refl a) zero_lt_one ⟩ } + +instance linear_ordered_field.to_no_bot_order [linear_ordered_field α] : no_bot_order α := +{ no_bot := assume a, ⟨a + -1, + add_lt_of_le_of_neg (le_refl _) (neg_lt_of_neg_lt $ by simp [zero_lt_one]) ⟩ } + end section diff --git a/algebra/group.lean b/algebra/group.lean index 4664c65f97269..f6bc547b9e611 100644 --- a/algebra/group.lean +++ b/algebra/group.lean @@ -184,6 +184,9 @@ lemma abs_le_iff : abs a ≤ b ↔ (- b ≤ a ∧ a ≤ b) := ⟨assume h, ⟨neg_le_of_neg_le $ le_trans (neg_le_abs_self _) h, le_trans (le_abs_self _) h⟩, assume ⟨h₁, h₂⟩, abs_le_of_le_of_neg_le h₂ $ neg_le_of_neg_le h₁⟩ +@[simp] lemma abs_eq_zero_iff : abs a = 0 ↔ a = 0 := +⟨eq_zero_of_abs_eq_zero, by simp [abs_zero] {contextual := tt}⟩ + end decidable_linear_ordered_comm_group /- diff --git a/data/rat.lean b/data/rat.lean index 4e62dd74d1cfd..859394577377d 100644 --- a/data/rat.lean +++ b/data/rat.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl Introduces the rational numbers as discrete, linear ordered field. -/ -import data.nat.gcd data.pnat data.int.basic pending +import data.nat.gcd data.pnat data.int.basic order.basic pending /- linorder -/ diff --git a/order/basic.lean b/order/basic.lean index c1d556faeccc8..10d3d34478789 100644 --- a/order/basic.lean +++ b/order/basic.lean @@ -111,3 +111,45 @@ theorem monotone_app (f : β → α → γ) (b : β) (m : monotone (λa b, f b a assume a a' h, m h b end monotone + +/- additional order classes -/ + +/-- order without a top element; somtimes called cofinal -/ +class no_top_order (α : Type u) [preorder α] : Prop := +(no_top : ∀a:α, ∃a', a < a') + +lemma no_top [preorder α] [no_top_order α] : ∀a:α, ∃a', a < a' := +no_top_order.no_top _ + +/-- order without a bottom element; somtimes called coinitial or dense -/ +class no_bot_order (α : Type u) [preorder α] : Prop := +(no_bot : ∀a:α, ∃a', a' < a) + +lemma no_bot [preorder α] [no_bot_order α] : ∀a:α, ∃a', a' < a := +no_bot_order.no_bot _ + +class densely_ordered (α : Type u) [preorder α] : Prop := +(dense : ∀a₁ a₂:α, a₁ < a₂ → ∃a, a₁ < a ∧ a < a₂) + +lemma dense [preorder α] [densely_ordered α] : ∀{a₁ a₂:α}, a₁ < a₂ → ∃a, a₁ < a ∧ a < a₂ := +densely_ordered.dense + +lemma le_of_forall_le [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀a₃>a₂, a₁ ≤ a₃) : + a₁ ≤ a₂ := +le_of_not_gt $ assume ha, + let ⟨a, ha₁, ha₂⟩ := dense ha in + lt_irrefl a $ lt_of_lt_of_le ‹a < a₁› (h _ ‹a₂ < a›) + +lemma eq_of_le_of_forall_le [linear_order α] [densely_ordered α] {a₁ a₂ : α} + (h₁ : a₂ ≤ a₁) (h₂ : ∀a₃>a₂, a₁ ≤ a₃) : a₁ = a₂ := +le_antisymm (le_of_forall_le h₂) h₁ + +lemma le_of_forall_ge [linear_order α] [densely_ordered α] {a₁ a₂ : α}(h : ∀a₃0, principal {p:α×α | dist p.1 p.2 < ε})) + +variables [metric_space α] + +def dist : α → α → ℝ := metric_space.dist + +@[simp] lemma dist_self (x : α) : dist x x = 0 := metric_space.dist_self x + +lemma eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y := +metric_space.eq_of_dist_eq_zero + +lemma dist_comm (x y : α) : dist x y = dist y x := metric_space.dist_comm x y + +@[simp] lemma dist_eq_zero_iff {x y : α} : dist x y = 0 ↔ x = y := +iff.intro eq_of_dist_eq_zero (assume : x = y, this ▸ dist_self _) + +@[simp] lemma zero_eq_dist_iff {x y : α} : 0 = dist x y ↔ x = y := +by rw [eq_comm, dist_eq_zero_iff] + +lemma dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z := +metric_space.dist_triangle x y z + +lemma uniformity_dist : uniformity = (⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε}) := +metric_space.uniformity_dist _ + +lemma uniformity_dist' : uniformity = (⨅ε:{ε:ℝ // ε>0}, principal {p:α×α | dist p.1 p.2 < ε.val}) := +by simp [infi_subtype]; exact uniformity_dist + +lemma dist_nonneg {x y : α} : 0 ≤ dist x y := +have 2 * dist x y ≥ 0, + from calc 2 * dist x y = dist x y + dist y x : by rw [dist_comm x y]; simp [bit0, bit1, mul_add] + ... ≥ 0 : by rw [←(dist_self x)]; apply dist_triangle, +nonneg_of_mul_nonneg_left this two_pos + +lemma dist_pos_of_ne {x y : α} (h : x ≠ y) : dist x y > 0 := +lt_of_le_of_ne dist_nonneg (by simp * at *) + +lemma 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, +lt_irrefl _ this + +lemma eq_of_forall_dist_le {x y : α} (h : ∀ε, ε > 0 → dist x y ≤ ε) : x = y := +eq_of_dist_eq_zero (eq_of_le_of_forall_le dist_nonneg h) + +instance metric_space.to_separated [metric_space α] : separated α := +set.ext $ assume ⟨x, y⟩, + begin + constructor, + simp [id_rel, separation_rel, uniformity_dist'], + exact (assume h, eq_of_forall_dist_le $ assume ε hε, + have (x, y) ∈ {p:α×α| dist p.1 p.2 < ε}, from h _ $ mem_infi_sets ⟨ε, hε⟩ $ subset.refl _, + le_of_lt this), + simp [id_rel, separation_rel] {contextual := tt}, + have h : principal {(y, y)} ≤ (@uniformity α _), + { rw [uniformity_dist], + exact (le_infi $ assume ε, le_infi $ assume hε, by simp; assumption) }, + exact (assume _ t ht, have {(y, y)} ⊆ t, from h ht, by simp at this; assumption) + end + +/- instantiate reals -/ +instance : metric_space ℝ := +{ real.uniform_space with + dist := λx y, abs (x - y), + dist_self := by simp [abs_zero], + eq_of_dist_eq_zero := by simp [add_eq_iff_eq_add_neg] {contextual := tt}, + dist_comm := assume x y, by rw [abs_sub], + dist_triangle := assume x y z, abs_sub_le _ _ _, + uniformity_dist := le_antisymm + (le_infi $ assume ε, le_infi $ assume hε, le_principal_iff.mpr $ mem_uniformity_real_iff.mpr $ + let ⟨q, hq₁, hq₂⟩ := exists_pos_of_rat hε in + ⟨q, hq₁, assume r₁ r₂ hr, lt_trans hr hq₂⟩) + (assume s hs, + let ⟨q, hq₁, hq₂⟩ := mem_uniformity_real_iff.mp hs in + mem_infi_sets (of_rat q) $ mem_infi_sets (of_rat_lt_of_rat.mpr hq₁) $ + assume ⟨r₁, r₂⟩, hq₂ r₁ r₂) } + +lemma uniform_continuous_dist' : uniform_continuous (λp:α×α, dist p.1 p.2) := +let i : {ε:ℝ // ε>0} := ⟨1, zero_lt_one⟩ in +have d : ∀p₁ p₂ q₁ q₂:α, dist p₁ q₁ - dist p₂ q₂ ≤ dist p₁ p₂ + dist q₁ q₂, + from assume p₁ p₂ q₁ q₂, + have dist p₁ q₁ ≤ (dist p₁ p₂ + dist q₁ q₂) + dist p₂ q₂, + from calc dist p₁ q₁ ≤ dist p₁ p₂ + dist p₂ q₁ : dist_triangle _ _ _ + ... ≤ dist p₁ p₂ + (dist p₂ q₂ + dist q₂ q₁) : add_le_add_left (dist_triangle _ _ _) _ + ... = _ : by simp [dist_comm], + sub_le_iff_le_add.mpr this, +have ∀{ε} {p₁ p₂ q₁ q₂ : α}, + ε > 0 → dist p₁ p₂ < ε / 2 ∧ dist q₁ q₂ < ε / 2 → dist (dist p₁ q₁) (dist p₂ q₂) < ε, + from assume ε p₁ p₂ q₁ q₂ hε ⟨h₁, h₂⟩, + have d₁ : dist p₁ q₁ - dist p₂ q₂ ≤ dist p₁ p₂ + dist q₁ q₂, from d _ _ _ _, + have d₂ : dist p₂ q₂ - dist p₁ q₁ ≤ dist p₁ p₂ + dist q₁ q₂, + by have h := d p₂ p₁ q₂ q₁; simp [dist_comm] at h; simp [dist_comm, h], + calc dist (dist p₁ q₁) (dist p₂ q₂) ≤ dist p₁ p₂ + dist q₁ q₂ : + abs_le_of_le_of_neg_le d₁ (by rw [neg_sub]; exact d₂) + ... < ε / 2 + ε / 2 : add_lt_add h₁ h₂ + ... = (ε + ε) / 2 : by simp [div_add_div_same] + ... = ε : add_self_div_two ε, +begin + rw [uniform_continuous, uniformity_prod_eq_prod, uniformity_dist', uniformity_dist], + simp [prod_infi_left i, prod_infi_right i, prod_principal_principal], + exact (tendsto_map' $ tendsto_infi $ assume ε, tendsto_infi $ assume hε, + let ε' : subtype {r : ℝ | r > 0} := ⟨ε / 2, div_pos_of_pos_of_pos hε two_pos⟩ in + tendsto_infi' ε' $ tendsto_infi' ε' $ tendsto_principal_principal $ + assume ⟨⟨p₁, p₂⟩, ⟨q₁, q₂⟩⟩, by simp; exact this hε), +end + +lemma uniform_continuous_dist [uniform_space β] {f g : β → α} + (hf : uniform_continuous f) (hg : uniform_continuous g) : + uniform_continuous (λb, dist (f b) (g b)) := +uniform_continuous_compose (uniform_continuous_prod_mk hf hg) uniform_continuous_dist' + +lemma continuous_dist' : continuous (λp:α×α, dist p.1 p.2) := +continuous_of_uniform uniform_continuous_dist' + +lemma continuous_dist [topological_space β] {f g : β → α} + (hf : continuous f) (hg : continuous g) : continuous (λb, dist (f b) (g b)) := +continuous_compose (continuous_prod_mk hf hg) continuous_dist' + +lemma tendsto_dist {f g : β → α} {x : filter β} {a b : α} + (hf : tendsto f x (nhds a)) (hg : tendsto g x (nhds b)) : + tendsto (λx, dist (f x) (g x)) x (nhds (dist a b)) := +have tendsto (λp:α×α, dist p.1 p.2) (nhds (a, b)) (nhds (dist a b)), + from continuous_iff_tendsto.mp continuous_dist' (a, b), +tendsto_compose (tendsto_prod_mk hf hg) (by rw [nhds_prod_eq] at this; exact this) + +/- instantiate metric space as a topology -/ +variables {x y z : α} {ε ε₁ ε₂ : ℝ} {s : set α} + +def open_ball (x : α) (ε : ℝ) : set α := {y | dist y x < ε} +def closed_ball (x : α) (ε : ℝ) := {y | dist y x ≤ ε} + +theorem open_ball_eq_empty_of_nonpos (hε : ε ≤ 0) : open_ball x ε = ∅ := +eq_empty_of_forall_not_mem $ assume y hy, + have dist y x < 0, from lt_of_lt_of_le hy hε, + lt_irrefl 0 (lt_of_le_of_lt dist_nonneg this) + +theorem pos_of_mem_open_ball (hy : y ∈ open_ball x ε) : ε > 0 := +lt_of_le_of_lt dist_nonneg hy + +theorem mem_open_ball (h : ε > 0) : x ∈ open_ball x ε := +show dist x x < ε, by rewrite dist_self; assumption + +theorem is_open_open_ball : is_open (open_ball x ε) := +is_open_lt (continuous_dist continuous_id continuous_const) continuous_const + +theorem is_closed_closed_ball : is_closed (closed_ball x ε) := +is_closed_le (continuous_dist continuous_id continuous_const) continuous_const + +lemma open_ball_subset_open_ball_of_le (h : ε₁ ≤ ε₂) : open_ball x ε₁ ⊆ open_ball x ε₂ := +assume y, assume ymem, lt_of_lt_of_le ymem h + +theorem nhds_eq_metric : nhds x = (⨅ε:{ε:ℝ // ε>0}, principal (open_ball x ε.val)) := +begin + rw [nhds_eq_uniformity, uniformity_dist', lift'_infi], + apply congr_arg, apply funext, intro ε, + rw [lift'_principal], + simp [open_ball, dist_comm], + exact monotone_preimage, + exact ⟨⟨1, zero_lt_one⟩⟩, + exact assume a b, rfl +end + +theorem mem_nhds_sets_iff_metric : s ∈ (nhds x).sets ↔ ∃ε>0, open_ball x ε ⊆ s := +begin + rw [nhds_eq_metric, infi_sets_eq], + simp [exists_subtype], + exact assume ⟨x, hx⟩ ⟨y, hy⟩, ⟨⟨min x y, lt_min hx hy⟩, + begin + simp, + constructor, + exact open_ball_subset_open_ball_of_le (min_le_left _ _), + exact open_ball_subset_open_ball_of_le (min_le_right _ _) + end⟩, + exact ⟨⟨1, zero_lt_one⟩⟩, +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] + +/- +theorem is_closed_metric : is_closed s ↔ (∀x, (∀ε>0, open_ball x ε ∩ s ≠ ∅) → x ∈ s := +_ + +theorem uniform_continuous_metric_iff [metric_space β] {f : α → β} : + uniform_continuous f ↔ (∀ε>0, ∃δ>0, ∀x y:α, dist x y < ε → dist (f x) (f y) < δ) := +_ + +theorem continuous_metric_iff [metric_space β] {f : α → β} : + continuous f ↔ (∀x:α, ∀ε>0, ∃δ>0, ∀y, dist x y < ε → dist (f x) (f y) < δ) := +_ +-/ diff --git a/topology/real.lean b/topology/real.lean index 2806843621584..afac3d4e35646 100644 --- a/topology/real.lean +++ b/topology/real.lean @@ -42,10 +42,6 @@ lemma one_lt_two : 1 < (2 : ℚ) := calc (1:ℚ) < 1 + 1 : lt_add_of_le_of_pos (le_refl 1) zero_lt_one ... = _ : by simp [bit0] -lemma zero_lt_two : 0 < (2 : ℚ) := -calc (0:ℚ) < 1 + 1 : lt_add_of_le_of_pos zero_le_one zero_lt_one - ... = _ : by simp [bit0] - /- rational numbers form a topological group and hence a uniform space -/ def zero_nhd : filter ℚ := (⨅r > 0, principal {q | abs q < r}) @@ -80,7 +76,7 @@ tendsto_zero_nhds $ assume i hi, by simp [abs_neg, mem_zero_nhd hi] lemma tendsto_add_rat_zero : tendsto (λp:ℚ×ℚ, p.1 + p.2) (filter.prod zero_nhd zero_nhd) zero_nhd := tendsto_zero_nhds $ assume i hi, -have 0 < i / 2, from div_pos_of_pos_of_pos hi zero_lt_two, +have 0 < i / 2, from div_pos_of_pos_of_pos hi two_pos, show {x : ℚ × ℚ | abs (x.1 + x.2) < i} ∈ (filter.prod zero_nhd zero_nhd).sets, from filter.upwards_sets _ (prod_mem_prod (mem_zero_nhd this) (mem_zero_nhd this)) $ assume ⟨a, b⟩ ⟨ha, hb⟩, @@ -635,7 +631,7 @@ lemma eq_0_of_nonneg_of_neg_nonneg {r : ℝ} (hp : r ∈ nonneg) (hn : -r ∈ no let d := lift_rat_fun (λq, q * (1 / 2)) in have uniform_continuous (λq:ℚ, q * (1 / 2)), from uniform_continuous_of_embedding $ uniform_embedding_mul_rat $ - ne_of_gt $ div_pos_of_pos_of_pos zero_lt_one zero_lt_two, + ne_of_gt $ div_pos_of_pos_of_pos zero_lt_one two_pos, have c_d : continuous d, from continuous_of_uniform $ uniform_continuous_uniformly_extend uniform_embedding_of_rat dense_embedding_of_rat.dense $ @@ -853,7 +849,7 @@ lemma mem_uniformity_real_iff {s : set (ℝ × ℝ)} : end, ⟨e, he, assume r₁ r₂ hr, hss' $ this (r₁, r₂) hr⟩, assume ⟨e, he, (hes : ∀ (r₁ r₂ : ℝ), abs (r₁ - r₂) < of_rat e → (r₁, r₂) ∈ s)⟩, - have 0 < e/2, from div_pos_of_pos_of_pos he zero_lt_two, + have 0 < e/2, from div_pos_of_pos_of_pos he two_pos, have {q:ℚ×ℚ | abs (q.1 - q.2) < e/2 } ∈ (uniformity.vmap (λp:ℚ×ℚ, (of_rat p.1, of_rat p.2))).sets, by rw [uniform_embedding_of_rat.right]; exact mem_uniformity_rat this, let ⟨t, ht, hte⟩ := this in @@ -870,7 +866,7 @@ lemma mem_uniformity_real_iff {s : set (ℝ × ℝ)} : assume p hp, have abs (p.1 - p.2) < of_rat e, from calc _ ≤ of_rat (e / 2) : this p hp - ... < of_rat e : of_rat_lt_of_rat.mpr $ div_lt_of_mul_lt_of_pos zero_lt_two $ + ... < of_rat e : of_rat_lt_of_rat.mpr $ div_lt_of_mul_lt_of_pos two_pos $ lt_mul_of_gt_one_right he two_gt_one, have (p.1, p.2) ∈ s, from hes _ _ this, @@ -904,7 +900,7 @@ have ∀a ∈ u ∩ of_rat '' {q : ℚ | 0 ≤ q}, a - of_rat i ∈ nonneg, have r - of_rat i ∈ nonneg, from @mem_closure_of_continuous _ _ _ _ (λr, r - of_rat i) _ (u ∩ of_rat '' {q | 0 ≤ q}) _ (continuous_sub continuous_id continuous_const) ‹r ∈ closure (u ∩ of_rat '' {q | 0 ≤ q})› this, -⟨i / 2, div_pos_of_pos_of_pos hi zero_lt_two, +⟨i / 2, div_pos_of_pos_of_pos hi two_pos, lt_of_lt_of_le (of_rat_lt_of_rat.mpr $ div_two_lt_of_pos hi) this⟩ lemma continuous_mul_real : continuous (λp:ℝ×ℝ, p.1 * p.2) := diff --git a/topology/uniform_space.lean b/topology/uniform_space.lean index 4ae4a797db7b8..c3ff656f0664c 100644 --- a/topology/uniform_space.lean +++ b/topology/uniform_space.lean @@ -58,7 +58,7 @@ lemma prod_mk_mem_comp_rel {a b c : α} {s t : set (α×α)} (h₁ : (a, c) ∈ ⟨c, h₁, h₂⟩ @[simp] lemma id_comp_rel {r : set (α×α)} : comp_rel id_rel r = r := -set.ext $ assume ⟨a, b⟩, ⟨assume ⟨a', heq, ha'⟩, +set.ext $ assume ⟨a, b⟩, ⟨assume ⟨a', heq, ha'⟩, (show a' = a, from heq.symm) ▸ ha', assume ha, ⟨a, rfl, ha⟩⟩ @@ -698,7 +698,7 @@ lemma totally_bounded_iff_filter {s : set α} : have f ≤ principal s, from infi_le_of_le ⟨∅, finite.empty⟩ $ by simp; exact subset.refl s, let ⟨c, (hc₁ : c ≤ f), (hc₂ : cauchy c)⟩ := h f ‹f ≠ ⊥› this, - ⟨m, hm, (hmd : set.prod m m ⊆ d)⟩ := (@mem_prod_same_iff α d c).mp $ hc₂.right hd + ⟨m, hm, (hmd : set.prod m m ⊆ d)⟩ := (@mem_prod_same_iff α c d).mp $ hc₂.right hd in have c ≤ principal s, from le_trans ‹c ≤ f› this, have m ∩ s ∈ c.sets, from inter_mem_sets hm $ le_principal_iff.mp this, @@ -1410,6 +1410,15 @@ lemma uniformity_prod [uniform_space α] [uniform_space β] : vmap (λp:(α×β)×(α×β), (p.1.2, p.2.2)) uniformity := by rw [prod.uniform_space, uniform_space.of_core_eq_to_core, uniformity, sup_uniformity]; refl +lemma uniformity_prod_eq_prod [uniform_space α] [uniform_space β] : + @uniformity (α×β) _ = + map (λp:(α×α)×(β×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) (filter.prod uniformity uniformity) := +have map (λp:(α×α)×(β×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) = + vmap (λp:(α×β)×(α×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))), + from funext $ assume f, map_eq_vmap_of_inverse + (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl) (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl), +by rw [this, uniformity_prod, prod_def, vmap_inf, vmap_vmap_comp, vmap_vmap_comp] + lemma mem_uniform_prod [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set (α × α)} {b : set (β × β)} (ha : a ∈ (@uniformity α _).sets) (hb : b ∈ (@uniformity β _).sets) : {p:(α×β)×(α×β) | (p.1.1, p.2.1) ∈ a ∧ (p.1.2, p.2.2) ∈ b } ∈ (@uniformity (α × β) _).sets := From 1f992c929dade0a34f07a35cad733da5692b4434 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Sun, 27 Aug 2017 12:26:42 -0400 Subject: [PATCH 4/4] fix(.): adapt to Lean changes: type class parameters to structures are now type class parameters in the projections and constructor --- algebra/module.lean | 6 +++--- data/fp/basic.lean | 2 +- order/basic.lean | 4 ++-- topology/topological_space.lean | 12 ++++++------ topology/topological_structures.lean | 16 ++++++++-------- 5 files changed, 20 insertions(+), 20 deletions(-) diff --git a/algebra/module.lean b/algebra/module.lean index 77b1a5335dd01..4371dbd9b750f 100644 --- a/algebra/module.lean +++ b/algebra/module.lean @@ -25,9 +25,9 @@ section module variables {α : Type u} {β : Type v} [ring α] [module α β] variables {a b c : α} {u v w : β} -theorem smul_left_distrib : a • (u + v) = a • u + a • v := module.smul_left_distrib _ a u v -theorem smul_right_distrib : (a + b) • u = a • u + b • u := module.smul_right_distrib _ a b u -theorem mul_smul : (a * b) • u = a • (b • u) := module.mul_smul _ a b u +theorem smul_left_distrib : a • (u + v) = a • u + a • v := module.smul_left_distrib a u v +theorem smul_right_distrib : (a + b) • u = a • u + b • u := module.smul_right_distrib a b u +theorem mul_smul : (a * b) • u = a • (b • u) := module.mul_smul a b u @[simp] theorem one_smul : (1 : α) • u = u := module.one_smul _ u @[simp] theorem zero_smul : (0 : α) • u = 0 := diff --git a/data/fp/basic.lean b/data/fp/basic.lean index 8fa853a16f80e..c7ad05998d4c3 100644 --- a/data/fp/basic.lean +++ b/data/fp/basic.lean @@ -183,7 +183,7 @@ namespace float variable [S : fpsettings] -def default_nan : float := nan (fpsettings.default_nan C) +def default_nan : float := nan fpsettings.default_nan instance : has_neg float := ⟨float.neg⟩ diff --git a/order/basic.lean b/order/basic.lean index 10d3d34478789..c4ae8fa285609 100644 --- a/order/basic.lean +++ b/order/basic.lean @@ -119,14 +119,14 @@ class no_top_order (α : Type u) [preorder α] : Prop := (no_top : ∀a:α, ∃a', a < a') lemma no_top [preorder α] [no_top_order α] : ∀a:α, ∃a', a < a' := -no_top_order.no_top _ +no_top_order.no_top /-- order without a bottom element; somtimes called coinitial or dense -/ class no_bot_order (α : Type u) [preorder α] : Prop := (no_bot : ∀a:α, ∃a', a' < a) lemma no_bot [preorder α] [no_bot_order α] : ∀a:α, ∃a', a' < a := -no_bot_order.no_bot _ +no_bot_order.no_bot class densely_ordered (α : Type u) [preorder α] : Prop := (dense : ∀a₁ a₂:α, a₁ < a₂ → ∃a, a₁ < a ∧ a < a₂) diff --git a/topology/topological_space.lean b/topology/topological_space.lean index 786b07e651e99..51b530c22ea38 100644 --- a/topology/topological_space.lean +++ b/topology/topological_space.lean @@ -512,7 +512,7 @@ class t1_space (α : Type u) [topological_space α] := (t1 : ∀x, is_closed ({x} : set α)) lemma is_closed_singleton [t1_space α] {x : α} : is_closed ({x} : set α) := -t1_space.t1 _ x +t1_space.t1 x lemma compl_singleton_mem_nhds [t1_space α] {x y : α} (h : y ≠ x) : - {x} ∈ (nhds y).sets := mem_nhds_sets is_closed_singleton $ by simp; exact h @@ -524,9 +524,9 @@ closure_eq_of_is_closed is_closed_singleton class t2_space (α : Type u) [topological_space α] := (t2 : ∀x y, x ≠ y → ∃u v : set α, is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ u ∩ v = ∅) -lemma t2_separation [t2_space α] {x y : α} (h : x ≠ y) : +lemma t2_separation [t2_space α] {x y : α} (h : x ≠ y) : ∃u v : set α, is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ u ∩ v = ∅ := -t2_space.t2 _ _ _ h +t2_space.t2 x y h instance t2_space.t1_space [topological_space α] [t2_space α] : t1_space α := ⟨assume x, @@ -546,7 +546,7 @@ instance t2_space.t1_space [topological_space α] [t2_space α] : t1_space α := lemma eq_of_nhds_neq_bot [ht : t2_space α] {x y : α} (h : nhds x ⊓ nhds y ≠ ⊥) : x = y := classical.by_contradiction $ assume : x ≠ y, -let ⟨u, v, hu, hv, hx, hy, huv⟩ := t2_space.t2 _ x y this in +let ⟨u, v, hu, hv, hx, hy, huv⟩ := t2_space.t2 x y this in have u ∩ v ∈ (nhds x ⊓ nhds y).sets, from inter_mem_inf_sets (mem_nhds_sets hu hx) (mem_nhds_sets hv hy), h $ empty_in_sets_eq_bot.mp $ huv ▸ this @@ -723,8 +723,8 @@ instance inhabited_topological_space {α : Type u} : inhabited (topological_spac ⟨⊤⟩ lemma t2_space_top : @t2_space α ⊤ := -⟨assume x y hxy, ⟨{x}, {y}, trivial, trivial, mem_insert _ _, mem_insert _ _, - eq_empty_of_forall_not_mem $ by intros z hz; simp at hz; cc⟩⟩ +{ t2 := assume x y hxy, ⟨{x}, {y}, trivial, trivial, mem_insert _ _, mem_insert _ _, + eq_empty_of_forall_not_mem $ by intros z hz; simp at hz; cc⟩ } lemma le_of_nhds_le_nhds {t₁ t₂ : topological_space α} (h : ∀x, @nhds α t₂ x ≤ @nhds α t₁ x) : t₁ ≤ t₂ := diff --git a/topology/topological_structures.lean b/topology/topological_structures.lean index 1f8e92f188183..6155e7f17cdab 100644 --- a/topology/topological_structures.lean +++ b/topology/topological_structures.lean @@ -27,7 +27,7 @@ class topological_add_monoid (α : Type u) [topological_space α] [add_monoid α variables [topological_space α] [add_monoid α] lemma continuous_add' [topological_add_monoid α] : continuous (λp:α×α, p.1 + p.2) := -topological_add_monoid.continuous_add _ _ +topological_add_monoid.continuous_add α lemma continuous_add [topological_add_monoid α] [topological_space β] {f : β → α} {g : β → α} (hf : continuous f) (hg : continuous g) : continuous (λx, f x + g x) := @@ -36,7 +36,7 @@ continuous_compose (continuous_prod_mk hf hg) continuous_add' lemma tendsto_add [topological_add_monoid α] {f : β → α} {g : β → α} {x : filter β} {a b : α} (hf : tendsto f x (nhds a)) (hg : tendsto g x (nhds b)) : tendsto (λx, f x + g x) x (nhds (a + b)) := have tendsto (λp:α×α, p.fst + p.snd) (nhds (a, b)) (nhds (a + b)), - from continuous_iff_tendsto.mp (topological_add_monoid.continuous_add _ _) (a, b), + from continuous_iff_tendsto.mp (topological_add_monoid.continuous_add α) (a, b), tendsto_compose (tendsto_prod_mk hf hg) (by rw [nhds_prod_eq] at this; exact this) end topological_add_monoid @@ -49,7 +49,7 @@ class topological_add_group (α : Type u) [topological_space α] [add_group α] variables [topological_space α] [add_group α] lemma continuous_neg' [topological_add_group α] : continuous (λx:α, - x) := -topological_add_group.continuous_neg _ _ +topological_add_group.continuous_neg α lemma continuous_neg [topological_add_group α] [topological_space β] {f : β → α} (hf : continuous f) : continuous (λx, - f x) := @@ -57,7 +57,7 @@ continuous_compose hf continuous_neg' lemma tendsto_neg [topological_add_group α] {f : β → α} {x : filter β} {a : α} (hf : tendsto f x (nhds a)) : tendsto (λx, - f x) x (nhds (- a)) := -tendsto_compose hf (continuous_iff_tendsto.mp (topological_add_group.continuous_neg _ _) a) +tendsto_compose hf (continuous_iff_tendsto.mp (topological_add_group.continuous_neg α) a) lemma continuous_sub [topological_add_group α] [topological_space β] {f : β → α} {g : β → α} (hf : continuous f) (hg : continuous g) : continuous (λx, f x - g x) := @@ -78,12 +78,12 @@ variables [topological_space α] [ring α] lemma continuous_mul [topological_ring α] [topological_space β] {f : β → α} {g : β → α} (hf : continuous f) (hg : continuous g) : continuous (λx, f x * g x) := -continuous_compose (continuous_prod_mk hf hg) (topological_ring.continuous_mul _ _) +continuous_compose (continuous_prod_mk hf hg) (topological_ring.continuous_mul α) lemma tendsto_mul [topological_ring α] {f : β → α} {g : β → α} {x : filter β} {a b : α} (hf : tendsto f x (nhds a)) (hg : tendsto g x (nhds b)) : tendsto (λx, f x * g x) x (nhds (a * b)) := have tendsto (λp:α×α, p.fst * p.snd) (nhds (a, b)) (nhds (a * b)), - from continuous_iff_tendsto.mp (topological_ring.continuous_mul _ _) (a, b), + from continuous_iff_tendsto.mp (topological_ring.continuous_mul α) (a, b), tendsto_compose (tendsto_prod_mk hf hg) (by rw [nhds_prod_eq] at this; exact this) end topological_ring @@ -100,10 +100,10 @@ lemma order_separated {a₁ a₂ : α} (h : a₁ < a₂) : ∃u v : set α, is_open u ∧ is_open v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ (∀b₁∈u, ∀b₂∈v, b₁ < b₂) := match dense_or_discrete h with | or.inl ⟨a, ha₁, ha₂⟩ := ⟨{a' | a' < a}, {a' | a < a'}, - linear_ordered_topology.is_open_gt _ _ a, linear_ordered_topology.is_open_lt _ _ a, ha₁, ha₂, + linear_ordered_topology.is_open_gt a, linear_ordered_topology.is_open_lt a, ha₁, ha₂, assume b₁ h₁ b₂ h₂, lt_trans h₁ h₂⟩ | or.inr ⟨h₁, h₂⟩ := ⟨{a | a < a₂}, {a | a₁ < a}, - linear_ordered_topology.is_open_gt _ _ a₂, linear_ordered_topology.is_open_lt _ _ a₁, h, h, + linear_ordered_topology.is_open_gt a₂, linear_ordered_topology.is_open_lt a₁, h, h, assume b₁ hb₁ b₂ hb₂, calc b₁ ≤ a₁ : h₂ _ hb₁ ... < a₂ : h