Defs.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

9 declarations, 0 contain sorry, 0 declared as axioms

Measures having no atoms

Imports (4)

Imported by 3 files

def MeasureTheory.IsAtom An atom of a measure μ is a set s of positive measure for which all measurable subsets either have measure 0 or μ s line 32 source
Source documentation
An atom of a measure μ is a set s of positive measure for which all measurable subsets either have measure 0 or μ s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Set, MeasureTheory.Measure
Proof uses: And, LT.lt, ENNReal, OfNat.ofNat, LE.le, MeasurableSet, Or, Eq
8 instances, coercions and auxiliary constants left out.
```
def IsAtom (s : Set α) (μ : Measure α) :=
…
```
Mentions: s
class MeasureTheory.NoAtoms' Measure μ has no atoms if for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s line 38 source
Source documentation
Measure μ has no atoms if for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0, the converse is not true.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure
```
class NoAtoms' (μ : Measure α) : Prop where
…
```
theorem MeasureTheory.no_atoms_iff line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Iff, MeasureTheory.NoAtoms', Set, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, Exists, And, LE.le
Proof uses: Iff.intro, Not, MeasureTheory.IsAtom, MeasureTheory.NoAtoms'.no_atoms, Ne, Eq.mp, Or, Eq, forall_congr, implies_congr, Eq.refl, Eq.trans, Mathlib.Tactic.Push.not_and_eq, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Exists.intro, And.intro, Bot.bot, Eq.symm and 10 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.mk' line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, Exists, And, LE.le, MeasureTheory.NoAtoms'
Proof uses: Eq.mpr, id, Eq, congrArg, propext, MeasureTheory.no_atoms_iff, MeasureTheory.exists_measurable_superset, Exists.intro, Inter.inter, And.intro, Set.inter_subset_right, MeasurableSet.inter, le_antisymm, Eq.symm, MeasureTheory.measure_mono, Set.inter_subset_left, Trans.trans, rfl, eq_of_heq, HEq and 7 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.NoAtoms'.exists_measurable_subset_lt line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, Exists, And, LE.le
Proof uses: Iff.mp, MeasureTheory.no_atoms_iff
16 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.NoAtoms'.exists_measurable_subset_lt₀ line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasureTheory.NullMeasurableSet, LT.lt, ENNReal, OfNat.ofNat, Exists, And, LE.le, MeasurableSet
Proof uses: Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq, Eq.mpr, id, Eq, congrArg, Eq.symm, Filter.EventuallyEq.measure_eq, MeasureTheory.NoAtoms'.exists_measurable_subset_lt, Eq.mp, Exists.intro, And.intro, LE.le.trans
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.NoAtoms'.instNullSingletonClass line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', MeasurableSingletonClass, MeasureTheory.NullMeasurableSpace, MeasureTheory.NullSingletonClass
Proof uses: MeasureTheory.NullSingletonClass.mk, Decidable.byContradiction, Eq, ENNReal, Set, Singleton.singleton, OfNat.ofNat, Not, And, LE.le, MeasurableSet, LT.lt, Exists, False, MeasureTheory.NoAtoms'.exists_measurable_subset_lt₀, MeasureTheory.nullMeasurableSet_singleton, Eq.mp, Ne, Bot.bot, congrArg and 10 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.NoAtoms'.instNullSingletonClass' TODO: Do we really need SigmaFinite μ or is SFinite μ sufficient? line 115 source
Source comment
TODO: Do we really need `SigmaFinite μ` or is `SFinite μ` sufficient?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', MeasureTheory.SigmaFinite, MeasureTheory.NullSingletonClass
Proof uses: MeasureTheory.NullSingletonClass.mk, Decidable.byContradiction, Eq, ENNReal, Set, Singleton.singleton, OfNat.ofNat, Not, MeasureTheory.toMeasurable, MeasureTheory.IsAtom, And.intro, LT.lt, LE.le, MeasurableSet, Or, Eq.mp, Bot.bot, congrArg, Eq.symm, MeasureTheory.measure_toMeasurable and 25 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
instance instNullSingletonClass' [SigmaFinite μ] :
    NullSingletonClass μ where
…
```
lemma MeasureTheory.NoAtoms'.restrict line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.NoAtoms', Set, MeasureTheory.NullMeasurableSet, MeasureTheory.Measure.restrict
Proof uses: MeasureTheory.NoAtoms'.mk', MeasurableSet, LT.lt, ENNReal, OfNat.ofNat, Eq.mpr, Exists, And, LE.le, Inter.inter, id, Eq, congrArg, MeasureTheory.Measure.restrict_apply, MeasureTheory.NoAtoms'.exists_measurable_subset_lt₀, MeasureTheory.NullMeasurableSet.inter, MeasurableSet.nullMeasurableSet, Eq.mp, Exists.intro, And.intro and 6 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.