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 9 curated AI-written annotations and 485 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, Polynomial Freiman-Ruzsa proof paper, arXiv v2

26 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib.MeasureTheory.Measure.Map

Imported by 6 files

class FiniteRange The property of having a finite range line 8 source
Source documentation
The property of having a finite range.

no axioms what this means
```
class FiniteRange {Ω G : Type*} (X : Ω → G) : Prop where
…
```
abbrev FiniteRange.fintype fintype structure on the range of a finite range map line 12 source
Source documentation
fintype structure on the range of a finite range map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FiniteRange, Fintype, Set.range
Proof uses: Set.Finite.fintype, FiniteRange.finite
1 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev FiniteRange.fintype {Ω G : Type*} (X : Ω → G) [hX : FiniteRange X] :
    Fintype (Set.range X) := hX.finite.fintype
```
Mentions: FiniteRange
def FiniteRange.toFinset The range of a finite range map, as a finset line 16 source
Source documentation
The range of a finite range map, as a finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FiniteRange, Finset
Proof uses: Set.toFinset, Set.range, FiniteRange.fintype

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def FiniteRange.toFinset {Ω G : Type*} (X : Ω → G) [hX : FiniteRange X] : Finset G :=
…
```
Mentions: FiniteRange
instance (instance at line 20) line 20 source
Source documentation
If the codomain of X is finite, then X has finite range.
```
instance {Ω G : Type*} (X : Ω → G) [Finite G] : FiniteRange X where
…
```
Mentions: FiniteRange
example (example at line 23) line 23 source
lemma finiteRange_of_finset Functions ranging in a Finset have finite range line 26 source
Source documentation
Functions ranging in a Finset have finite range

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Membership.mem, FiniteRange
Proof uses: FiniteRange.mk, Set.Finite.subset, Finset.finite_toSet, Set.range, Set, Eq, Exists, Eq.mp
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma finiteRange_of_finset {Ω G : Type*} (f : Ω → G) (A : Finset G) (h : ∀ ω, f ω ∈ A) :
    FiniteRange f := by
…
```
Mentions: FiniteRange
lemma FiniteRange.range line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FiniteRange, Eq, Set, Set.range, Finset, FiniteRange.toFinset
Proof uses: of_eq_true, Eq.trans, True, congrArg, Set.coe_toFinset, FiniteRange.fintype, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FiniteRange.mem line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FiniteRange, Membership.mem, Finset, FiniteRange.toFinset
Proof uses: Eq.mpr, Set, id, Eq, Set.range, congrFun', congrArg, Eq.symm, FiniteRange.range, Exists, of_eq_true
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FiniteRange.mem_iff line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FiniteRange, Iff, Membership.mem, Finset, FiniteRange.toFinset, Exists, Eq
Proof uses: Eq.mpr, Set, id, congrFun', congrArg, Set.range, Eq.symm, FiniteRange.range, of_eq_true, Eq.trans, True, iff_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance (instance at line 48) line 48 source
Source documentation
Constants have finite range
```
instance {Ω G : Type*} (c : G) : FiniteRange (fun _ : Ω ↦ c) := by
…
```
Mentions: FiniteRange
instance (instance at line 53) line 53 source
Source documentation
If X has finite range, then any function of X has finite range.
```
instance {Ω G H : Type*} (X : Ω → G) (f : G → H) [hX : FiniteRange X] : FiniteRange (f ∘ X) where
…
```
Mentions: FiniteRange
instance (instance at line 57) line 57 source
Source documentation
If X has finite range, then X of any function has finite range.
```
instance {Ω Ω' G : Type*} (X : Ω → G) (f : Ω' → Ω) [hX : FiniteRange X] : FiniteRange (X ∘ f) := by
…
```
Mentions: FiniteRange

instance (instance at line 63) line 63 source

Source documentation

If X, Y have finite range, then so does the pair ⟨X, Y⟩.

instance {Ω G H : Type*} (X : Ω → G) (Y : Ω → H) [hX : FiniteRange X] [hY : FiniteRange Y] :
    FiniteRange fun ω ↦ (X ω, Y ω) where
…

Mentions: FiniteRange

instance FiniteRange.mul The sum of functions of finite range, has finite range line 69 source
Source documentation
The sum of functions of finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mul, FiniteRange, HMul.hMul
Proof uses: id, inferInstance, Function.comp, Prod, Prod.fst, Prod.snd, Prod.mk
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
instance FiniteRange.mul {Ω G : Type*} (X Y : Ω → G) [Mul G] [FiniteRange X] [FiniteRange Y] :
    FiniteRange (X * Y) := by
…
```
Mentions: FiniteRange
instance FiniteRange.mul' The sum of functions of finite range, has finite range line 76 source
Source documentation
The sum of functions of finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mul, FiniteRange, HMul.hMul
2 instances, coercions and auxiliary constants left out.
```
instance FiniteRange.mul' {Ω G : Type*} (X Y : Ω → G) [Mul G] [FiniteRange X] [FiniteRange Y] :
    FiniteRange fun ω ↦ X ω * Y ω := FiniteRange.mul ..
…
```
Mentions: FiniteRange, FiniteRange.mul
instance FiniteRange.div The difference of functions of finite range, has finite range line 81 source
Source documentation
The difference of functions of finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Div, FiniteRange, HDiv.hDiv
Proof uses: id, inferInstance, Function.comp, Prod, Prod.fst, Prod.snd, Prod.mk
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
instance FiniteRange.div {Ω G : Type*} (X Y : Ω → G) [Div G]
    [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (X/Y) := by
…
```
Mentions: FiniteRange
instance FiniteRange.div' The sum of functions of finite range, has finite range line 88 source
Source documentation
The sum of functions of finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Div, FiniteRange, HDiv.hDiv
2 instances, coercions and auxiliary constants left out.
```
instance FiniteRange.div' {Ω G : Type*} (X Y : Ω → G) [Div G] [FiniteRange X] [FiniteRange Y] :
    FiniteRange fun ω ↦ X ω / Y ω := FiniteRange.div ..
…
```
Mentions: FiniteRange, FiniteRange.div
instance FiniteRange.inv The negation of a function of finite range, has finite range line 93 source
Source documentation
The negation of a function of finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inv, FiniteRange, Inv.inv
Proof uses: id, inferInstance, Function.comp
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
instance FiniteRange.inv {Ω G : Type*} (X : Ω → G) [Inv G] [hX : FiniteRange X] :
    FiniteRange X⁻¹ := by
…
```
Mentions: FiniteRange
instance FiniteRange.inv' The sum of functions of finite range, has finite range line 100 source
Source documentation
The sum of functions of finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inv, FiniteRange, Inv.inv
1 instances, coercions and auxiliary constants left out.
```
instance FiniteRange.inv' {Ω G : Type*} (X : Ω → G) [Inv G] [FiniteRange X] :
    FiniteRange fun ω ↦ (X ω)⁻¹ := FiniteRange.inv _
…
```
Mentions: FiniteRange, FiniteRange.inv
instance FiniteRange.zpow The multiple of a function of finite range by a constant, has finite range line 105 source
Source documentation
The multiple of a function of finite range by a constant, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Pow, Int, FiniteRange, HPow.hPow
Proof uses: id, inferInstance, Function.comp
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
instance FiniteRange.zpow {Ω G : Type*} (X : Ω → G) [Pow G ℤ] [hX : FiniteRange X] (n : ℤ) :
    FiniteRange (X ^ n) := by
…
```
Mentions: FiniteRange
instance FiniteRange.zpow' The multiple of a function of finite range by a constant, has finite range line 112 source
Source documentation
The multiple of a function of finite range by a constant, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Pow, Int, FiniteRange, HPow.hPow
2 instances, coercions and auxiliary constants left out.
```
instance FiniteRange.zpow' {Ω G : Type*} (X : Ω → G) [Pow G ℤ] [FiniteRange X] (n : ℤ) :
    FiniteRange fun ω ↦ X ω ^ n := FiniteRange.zpow ..
…
```
Mentions: FiniteRange, FiniteRange.zpow
instance FiniteRange.finprod The sum of a finite number of functions with finite range, has finite range line 117 source
Source documentation
The sum of a finite number of functions with finite range, has finite range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Finset, FiniteRange, Finset.prod
Proof uses: Finset.induction_on, Classical.propDecidable, Eq, id, EmptyCollection.emptyCollection, OfNat.ofNat, inferInstance, Not, Membership.mem, Insert.insert, HMul.hMul, Finset.prod_insert, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
instance FiniteRange.finprod {Ω G I : Type*} [CommMonoid G] {s : Finset I} (X : I → Ω → G)
    [∀ i, FiniteRange (X i)] :
    FiniteRange (∏ i ∈ s, X i) := by
…
```
Mentions: FiniteRange
lemma FiniteRange.full line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.Measure, Eq, ENNReal, Set, MeasureTheory.Measure.map, Finset, FiniteRange.toFinset, Set.univ
Proof uses: Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, Finset.measurableSet, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, Exists and 1 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma FiniteRange.real_full line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.Measure, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Finset, FiniteRange.toFinset, Set.univ
Proof uses: of_eq_true, ENNReal.toReal, Set, ENNReal, Eq.trans, True, congrFun', congrArg, FiniteRange.full, eq_self
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FiniteRange.null_of_compl line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, FiniteRange, AEMeasurable, Eq, ENNReal, Set, MeasureTheory.Measure.map, Compl.compl, Finset, FiniteRange.toFinset, OfNat.ofNat
Proof uses: Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply₀, MeasureTheory.NullMeasurableSet, MeasurableSet.nullMeasurableSet, Finset.measurableSet, EmptyCollection.emptyCollection, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, Set.ext, of_eq_true, Iff, Membership.mem and 9 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma FiniteRange.ae_mem_toFinset line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, FiniteRange, AEMeasurable, Filter.Eventually, Membership.mem, Set, Finset, FiniteRange.toFinset, MeasureTheory.ae, MeasureTheory.Measure.map
Proof uses: FiniteRange.null_of_compl
5 instances, coercions and auxiliary constants left out.