From b5973ba9c9490c3e40b79b4337729439c45c3393 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 4 Jun 2022 17:34:17 +0000 Subject: [PATCH] feat(measure_theory/measure/measure_space): there exists a ball of positive measure (#14449) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Motivated by #12933 Co-authored-by: Mantas Bakšys --- src/measure_theory/measure/measure_space.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 27657aa96cd3c..600ffe9a8c022 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -2831,6 +2831,22 @@ lemma is_locally_finite_measure_of_is_finite_measure_on_compacts [topological_sp exact ⟨K, K_mem, K_compact.measure_lt_top⟩, end⟩ +lemma exists_pos_measure_of_cover [encodable ι] {U : ι → set α} (hU : (⋃ i, U i) = univ) + (hμ : μ ≠ 0) : ∃ i, 0 < μ (U i) := +begin + contrapose! hμ with H, + rw [← measure_univ_eq_zero, ← hU], + exact measure_Union_null (λ i, nonpos_iff_eq_zero.1 (H i)) +end + +lemma exists_pos_preimage_ball [pseudo_metric_space δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) : + ∃ n : ℕ, 0 < μ (f ⁻¹' metric.ball x n) := +exists_pos_measure_of_cover (by rw [← preimage_Union, metric.Union_ball_nat, preimage_univ]) hμ + +lemma exists_pos_ball [pseudo_metric_space α] (x : α) (hμ : μ ≠ 0) : + ∃ n : ℕ, 0 < μ (metric.ball x n) := +exists_pos_preimage_ball id x hμ + /-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space. -/ lemma null_of_locally_null [topological_space α] [second_countable_topology α]