Source indexedtheorem · leanprover/lean4:v4.32.0

Metric.secondCountableTopology_of_almost_dense_set_balls_nat

Carleson.ToMathlib.CoveredByBalls · Carleson/ToMathlib/CoveredByBalls.lean:153 to 165

Source documentation

A pseudometric space is second countable if, for every ε > 0 and every ball B with natural number radius around a given point x₀, there is a countable set which is ε-dense in B.

Exact Lean statement

theorem Metric.secondCountableTopology_of_almost_dense_set_balls_nat
    {α} [PseudoMetricSpace α] (x₀ : α)
    (H : ∀ ε > (0 : ℝ), ∀ (n : ℕ),
    ∃ s : Set α, s.Countable ∧ ∀ x ∈ ball x₀ n, ∃ y ∈ s, dist x y ≤ ε) :
    SecondCountableTopology α

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Metric.secondCountableTopology_of_almost_dense_set_balls_nat    {α} [PseudoMetricSpace α] (x₀ : α)    (H : ∀ ε > (0 : ℝ), ∀ (n : ℕ),    ∃ s : Set α, s.Countable ∧ ∀ x ∈ ball x₀ n, ∃ y ∈ s, dist x y ≤ ε) :    SecondCountableTopology α := by  apply secondCountable_of_almost_dense_set  intro ε hε  specialize H ε hε  choose s h1s y h1y h2y using H  use ⋃ n, s n, by simp [*]  intro x  use y (⌊dist x x₀⌋₊ + 1) x (by simp [Nat.lt_floor_add_one])  simpa only [Set.mem_iUnion, and_true, h2y] using ⟨_, h1y ..⟩