CoveredByBalls.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

20 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 2 files

lemma CoveredByBalls.mono_set line 24 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Nat, Real, CoveredByBalls, LE.le
Proof uses: Finset, Finset.card, Set.iUnion, Membership.mem, Metric.ball, CoveredByBalls.mk
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.mono_nat line 28 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Nat, Real, CoveredByBalls, LE.le
Proof uses: Finset, Finset.card, Set.iUnion, Membership.mem, Metric.ball, CoveredByBalls.mk, LE.le.trans
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.mono_real line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Nat, Real, CoveredByBalls, LE.le
Proof uses: Finset, Finset.card, Set.iUnion, Membership.mem, Metric.ball, CoveredByBalls.mk, LE.le.trans, Set.iUnion_mono'', Metric.ball_subset_ball
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.empty line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, CoveredByBalls, EmptyCollection.emptyCollection, Set
Proof uses: CoveredByBalls.mk, Finset, of_eq_true, LE.le, OfNat.ofNat, Set.iUnion, Membership.mem, Metric.ball, Eq.trans, True, congrArg, funext, False, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.zero_left line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Real, Iff, CoveredByBalls, OfNat.ofNat, Nat, Eq, EmptyCollection.emptyCollection
Proof uses: Iff.intro, Finset, LE.le, Finset.card, Set.iUnion, Membership.mem, Metric.ball, Eq.mp, Eq.trans, congrArg, funext, False, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty, Eq.symm, CoveredByBalls.empty
24 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.zero_right line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Nat, Iff, CoveredByBalls, OfNat.ofNat, Real, Eq, EmptyCollection.emptyCollection
Proof uses: Iff.intro, Finset, LE.le, Finset.card, Set.iUnion, Membership.mem, Metric.ball, Eq.mp, Eq.trans, congrArg, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Metric.ball_zero, Set.iUnion_empty, Eq.mpr, id, False, Set.iUnion_of_empty and 8 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.ball line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, CoveredByBalls, Metric.ball, OfNat.ofNat, Nat
Proof uses: Finset, Singleton.singleton, LE.le, Finset.card, le_refl, Set, Set.iUnion, Membership.mem, of_eq_true, Eq.trans, True, congrArg, Eq, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_iUnion_eq_left, CoveredByBalls.mk
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma CoveredByBalls.trans line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Nat, Real, CoveredByBalls, BallsCoverBalls, HMul.hMul
Proof uses: Finset, LE.le, Finset.card, Set.iUnion, Membership.mem, Metric.ball, Eq.mpr, Exists, And, id, Eq, congrArg, propext, coveredByBalls_iff, Iff.mp, Exists.intro, Finset.biUnion, Classical.propDecidable, Exists.choose, And.intro and 16 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma BallsCoverBalls.mono line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, BallsCoverBalls, LE.le
Proof uses: CoveredByBalls.mono_set, Metric.ball, Metric.ball_subset_ball
2 instances, coercions and auxiliary constants left out.
lemma BallsCoverBalls.trans line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, BallsCoverBalls, HMul.hMul
Proof uses: CoveredByBalls.trans, Metric.ball
2 instances, coercions and auxiliary constants left out.
lemma BallsCoverBalls.zero line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, BallsCoverBalls, OfNat.ofNat
Proof uses: Eq.mpr, CoveredByBalls, Metric.ball, EmptyCollection.emptyCollection, Set, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrFun', congrArg, Metric.ball_zero, eq_self, CoveredByBalls.empty
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma BallsCoverBalls.nonpos line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, LE.le, OfNat.ofNat, BallsCoverBalls
Proof uses: BallsCoverBalls.mono, BallsCoverBalls.zero
6 instances, coercions and auxiliary constants left out.
lemma AllBallsCoverBalls.mk Prove AllBallsCoverBalls only for balls of positive radius line 110 source
Source documentation
Prove AllBallsCoverBalls only for balls of positive radius.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, LE.le, OfNat.ofNat, GT.gt, BallsCoverBalls, HMul.hMul, AllBallsCoverBalls
Proof uses: LT.lt, Or, lt_or_ge, BallsCoverBalls.nonpos, mul_nonpos_of_nonneg_of_nonpos
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma mk {a : ℝ} (ha : 0 ≤ a) (h : ∀ r > 0, BallsCoverBalls X (a * r) r n) :
    AllBallsCoverBalls X a n := by
…
```
Mentions: BallsCoverBalls, AllBallsCoverBalls
lemma AllBallsCoverBalls.pow line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, AllBallsCoverBalls, HPow.hPow
Proof uses: Nat.recAux, BallsCoverBalls, HMul.hMul, Eq.mpr, OfNat.ofNat, id, Eq, congr, congrFun', congrArg, Eq.trans, pow_zero, one_mul, CoveredByBalls.ball, HAdd.hAdd, pow_succ, pow_succ', BallsCoverBalls.trans, Eq.mp, Eq.symm and 2 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma AllBallsCoverBalls.ballsCoverBalls_pow line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, AllBallsCoverBalls, BallsCoverBalls, HPow.hPow, OfNat.ofNat
Proof uses: BallsCoverBalls.mono, HMul.hMul, AllBallsCoverBalls.pow, Eq.mpr, LE.le, id, Eq, congrArg, mul_one, le_refl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma AllBallsCoverBalls.ballsCoverBalls line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, AllBallsCoverBalls, LT.lt, OfNat.ofNat, BallsCoverBalls, HPow.hPow, Nat.ceil, Real.logb, HDiv.hDiv
Proof uses: LE.le, Or, le_or_gt, BallsCoverBalls.nonpos, BallsCoverBalls.mono, HMul.hMul, AllBallsCoverBalls.pow, Trans.trans, Eq, Eq.mpr, id, congrArg, div_mul_cancel₀, LT.lt.ne', Eq.refl, mul_le_mul_of_nonneg_right, Real.le_pow_natCeil_logb, div_pos, le_of_lt
64 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Metric.secondCountableTopology_of_almost_dense_set_balls_nat Documented declaration: secondCountableTopology_of_almost_dense_set_balls_nat line 153 source
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, GT.gt, OfNat.ofNat, Nat, Exists, Set, And, Set.Countable, Membership.mem, Metric.ball, LE.le, Dist.dist, SecondCountableTopology
Proof uses: Metric.secondCountable_of_almost_dense_set, Exists.intro, Set.iUnion, And.intro, of_eq_true, Eq.trans, True, forall_congr, eq_true, And.left, implies_true, HAdd.hAdd, Nat.floor, LT.lt, congrFun', congrArg, Nat.cast_add, Nat.cast_one, Eq.mpr, id and 6 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: s
theorem Metric.secondCountableTopology_of_almost_dense_set_balls A pseudometric space is second countable if, for every ε > 0 and every ball B, there is a countable set which is ε-dense in B line 170 source
Source documentation
A pseudometric space is second countable if, for every ε > 0 and every ball B, there is a countable set which is ε-dense in B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, GT.gt, OfNat.ofNat, Exists, Set, And, Set.Countable, Membership.mem, Metric.ball, LE.le, Dist.dist, SecondCountableTopology
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Metric.secondCountableTopology_of_almost_dense_set_balls_nat, Inhabited.default, Lean.Elab.Tactic.nonempty_to_inhabited, Nat, Exists.intro, And.intro
24 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem Metric.secondCountableTopology_of_almost_dense_set_balls
    {α} [PseudoMetricSpace α]
    (H : ∀ (x₀ : α), ∀ ε > (0 : ℝ), ∀ r,
    ∃ s : Set α, s.Countable ∧ ∀ x ∈ ball x₀ r, ∃ y ∈ s, dist x y ≤ ε) :
    SecondCountableTopology α := by
…
```
Mentions: s
theorem BallsCoverBalls.secondCountableTopology A pseudometric space is second countable if, for every ε > 0 and every ball B is covered by finitely many balls of radius ε line 186 source
Source documentation
A pseudometric space is second countable if, for every ε > 0 and every ball B is covered by finitely many balls of radius ε.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, GT.gt, OfNat.ofNat, Exists, Nat, BallsCoverBalls, SecondCountableTopology
Proof uses: Metric.secondCountableTopology_of_almost_dense_set_balls, Set, And, Set.Countable, Membership.mem, Metric.ball, LE.le, Dist.dist, CoveredByBalls, Finset, Finset.card, Set.iUnion, Exists.intro, And.intro, Finset.countable_toSet, Eq.mp, Eq.trans, congrArg, funext, LT.lt.le
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem BallsCoverBalls.secondCountableTopology
    (H : ∀ ε > (0 : ℝ), ∀ r, ∃ n, BallsCoverBalls X r ε n) :
    SecondCountableTopology X := by
…
```
Mentions: BallsCoverBalls
lemma AllBallsCoverBalls.secondCountableTopology A pseudometric space is second countable if every ball of radius a * r is covered by b many balls of radius r line 200 source
Source documentation
A pseudometric space is second countable if every ball of radius a * r is covered by b many balls of radius r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, AllBallsCoverBalls, LT.lt, OfNat.ofNat, SecondCountableTopology
Proof uses: BallsCoverBalls.secondCountableTopology, GT.gt, Exists.intro, BallsCoverBalls, HPow.hPow, Nat.ceil, Real.logb, HDiv.hDiv, AllBallsCoverBalls.ballsCoverBalls
23 instances, coercions and auxiliary constants left out.
```
lemma AllBallsCoverBalls.secondCountableTopology {a : ℝ} (h : AllBallsCoverBalls X a n)
    (h2 : 1 < a) : SecondCountableTopology X :=
…
```
Mentions: AllBallsCoverBalls