From bfccd1b8ff105cb7de6a627f4a98303d0f0eb42c Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 3 Dec 2021 08:57:28 +0000 Subject: [PATCH] chore(topology/{metric_space,instances/real}): cleanup (#10577) * merge `real.ball_eq` and `real.ball_eq_Ioo` into `real.ball_eq_Ioo`; * merge `real.closed_ball_eq` and `real.closed_ball_eq_Icc` into `real.closed_ball_eq_Icc`; * add missing `real.Icc_eq_closed_ball`; * generalize lemmas about `*bounded_Ixx` so that they work for (indexed) products of conditionally complete linear orders. --- src/analysis/seminorm.lean | 2 +- src/measure_theory/measure/lebesgue.lean | 4 ++-- src/number_theory/liouville/basic.lean | 2 +- src/topology/instances/real.lean | 29 +++++++----------------- src/topology/metric_space/basic.lean | 20 ++++++++++++---- 5 files changed, 27 insertions(+), 30 deletions(-) diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean index 19c5a4f068c90..24d5639dc4898 100644 --- a/src/analysis/seminorm.lean +++ b/src/analysis/seminorm.lean @@ -526,7 +526,7 @@ begin { simpa only [s', f, set.mem_preimage, one_smul] }, obtain ⟨ε, hε₀, hε⟩ := (metric.nhds_basis_closed_ball.1 _).1 (is_open_iff_mem_nhds.1 hs' 1 one_mem), - rw real.closed_ball_eq at hε, + rw real.closed_ball_eq_Icc at hε, have hε₁ : 0 < 1 + ε := hε₀.trans (lt_one_add ε), have : (1 + ε)⁻¹ < 1, { rw inv_lt_one_iff, diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean index 1be452fbe249b..0e3c89765864b 100644 --- a/src/measure_theory/measure/lebesgue.lean +++ b/src/measure_theory/measure/lebesgue.lean @@ -67,11 +67,11 @@ ennreal.eq_top_of_forall_nnreal_le $ λ r, @[simp] lemma volume_ball (a r : ℝ) : volume (metric.ball a r) = of_real (2 * r) := -by rw [ball_eq, volume_Ioo, ← sub_add, add_sub_cancel', two_mul] +by rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel', two_mul] @[simp] lemma volume_closed_ball (a r : ℝ) : volume (metric.closed_ball a r) = of_real (2 * r) := -by rw [closed_ball_eq, volume_Icc, ← sub_add, add_sub_cancel', two_mul] +by rw [closed_ball_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel', two_mul] @[simp] lemma volume_emetric_ball (a : ℝ) (r : ℝ≥0∞) : volume (emetric.ball a r) = 2 * r := diff --git a/src/number_theory/liouville/basic.lean b/src/number_theory/liouville/basic.lean index 0d1d2eb417854..e634ee31d3aec 100644 --- a/src/number_theory/liouville/basic.lean +++ b/src/number_theory/liouville/basic.lean @@ -146,7 +146,7 @@ begin { exact λ a, one_le_pow_of_one_le ((le_add_iff_nonneg_left 1).mpr a.cast_nonneg) _ }, -- 2: the polynomial `fR` is Lipschitz at `α` -- as its derivative continuous; { rw mul_comm, - rw real.closed_ball_eq at hy, + rw real.closed_ball_eq_Icc at hy, -- apply the Mean Value Theorem: the bound on the derivative comes from differentiability. refine convex.norm_image_sub_le_of_norm_deriv_le (λ _ _, fR.differentiable_at) (λ y h, by { rw fR.deriv, exact hM _ h }) (convex_Icc _ _) hy (mem_Icc_iff_abs_le.mp _), diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean index 2806bda03a582..5cb6d3d1dacdd 100644 --- a/src/topology/instances/real.lean +++ b/src/topology/instances/real.lean @@ -85,16 +85,16 @@ theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball theorem preimage_closed_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl -theorem ball_eq (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ := -by rw [← preimage_ball, real.ball_eq, preimage_Ioo] +theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ := +by rw [← preimage_ball, real.ball_eq_Ioo, preimage_Ioo] -theorem closed_ball_eq (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ := -by rw [← preimage_closed_ball, real.closed_ball_eq, preimage_Icc] +theorem closed_ball_eq_Icc (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ := +by rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc] instance : proper_space ℤ := ⟨ begin intros x r, - rw closed_ball_eq, + rw closed_ball_eq_Icc, exact (set.finite_Icc _ _).is_compact, end ⟩ @@ -144,7 +144,7 @@ instance : order_topology ℚ := induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _) instance : proper_space ℝ := -{ is_compact_closed_ball := λx r, by { rw real.closed_ball_eq, apply is_compact_Icc } } +{ is_compact_closed_ball := λx r, by { rw real.closed_ball_eq_Icc, apply is_compact_Icc } } instance : second_countable_topology ℝ := second_countable_of_proper @@ -239,15 +239,6 @@ real.continuous_mul.comp ((rat.continuous_coe_real.prod_map rat.continuous_coe_r instance : topological_ring ℚ := { continuous_mul := rat.continuous_mul, ..rat.topological_add_group } -theorem real.ball_eq_Ioo (x ε : ℝ) : ball x ε = Ioo (x - ε) (x + ε) := -set.ext $ λ y, by rw [mem_ball, real.dist_eq, - abs_sub_lt_iff, sub_lt_iff_lt_add', and_comm, sub_lt]; refl - -theorem real.Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2) := -by rw [real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, - add_sub_cancel', add_self_div_two, ← add_div, - add_assoc, add_sub_cancel'_right, add_self_div_two] - instance : complete_space ℝ := begin apply complete_of_cauchy_seq_tendsto, @@ -294,14 +285,10 @@ lemma real.bounded_iff_bdd_below_bdd_above {s : set ℝ} : bounded s ↔ bdd_bel ⟨begin assume bdd, rcases (bounded_iff_subset_ball 0).1 bdd with ⟨r, hr⟩, -- hr : s ⊆ closed_ball 0 r - rw real.closed_ball_eq at hr, -- hr : s ⊆ Icc (0 - r) (0 + r) + rw real.closed_ball_eq_Icc at hr, -- hr : s ⊆ Icc (0 - r) (0 + r) exact ⟨bdd_below_Icc.mono hr, bdd_above_Icc.mono hr⟩ end, -begin - intro h, - rcases bdd_below_bdd_above_iff_subset_Icc.1 h with ⟨m, M, I : s ⊆ Icc m M⟩, - exact (bounded_Icc m M).mono I -end⟩ +λ h, bounded_of_bdd_above_of_bdd_below h.2 h.1⟩ lemma real.subset_Icc_Inf_Sup_of_bounded {s : set ℝ} (h : bounded s) : s ⊆ Icc (Inf s) (Sup s) := diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 013170cbe67fd..8b1c70a2f4339 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -1020,17 +1020,27 @@ instance : order_topology ℝ := order_topology_of_nhds_abs $ λ x, by simp only [nhds_basis_ball.eq_binfi, ball, real.dist_eq, abs_sub_comm] -lemma real.ball_eq (x r : ℝ) : ball x r = Ioo (x - r) (x + r) := +lemma real.ball_eq_Ioo (x r : ℝ) : ball x r = Ioo (x - r) (x + r) := set.ext $ λ y, by rw [mem_ball, dist_comm, real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add', sub_lt] -lemma real.closed_ball_eq {x r : ℝ} : closed_ball x r = Icc (x - r) (x + r) := +lemma real.closed_ball_eq_Icc {x r : ℝ} : closed_ball x r = Icc (x - r) (x + r) := by ext y; rw [mem_closed_ball, dist_comm, real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add', sub_le] +theorem real.Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2) := +by rw [real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, + add_sub_cancel', add_self_div_two, ← add_div, + add_assoc, add_sub_cancel'_right, add_self_div_two] + +theorem real.Icc_eq_closed_ball (x y : ℝ) : Icc x y = closed_ball ((x + y) / 2) ((y - x) / 2) := +by rw [real.closed_ball_eq_Icc, ← sub_div, add_comm, ← sub_add, + add_sub_cancel', add_self_div_two, ← add_div, + add_assoc, add_sub_cancel'_right, add_self_div_two] + section metric_ordered -variables [conditionally_complete_linear_order α] [order_topology α] +variables [preorder α] [compact_Icc_space α] lemma totally_bounded_Icc (a b : α) : totally_bounded (Icc a b) := is_compact_Icc.totally_bounded @@ -1794,7 +1804,7 @@ lemma compact_space_iff_bounded_univ [proper_space α] : compact_space α ↔ bo section conditionally_complete_linear_order -variables [conditionally_complete_linear_order α] [order_topology α] +variables [preorder α] [compact_Icc_space α] lemma bounded_Icc (a b : α) : bounded (Icc a b) := (totally_bounded_Icc a b).bounded @@ -1996,7 +2006,7 @@ begin refine tendsto_cocompact_of_tendsto_dist_comp_at_top (0 : ℝ) _, simp only [filter.tendsto_at_top, eventually_cofinite, not_le, ← mem_ball], change ∀ r : ℝ, finite (coe ⁻¹' (ball (0 : ℝ) r)), - simp [real.ball_eq, set.finite_Ioo], + simp [real.ball_eq_Ioo, set.finite_Ioo], end end int