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

25 declarations, 0 contain sorry, 0 declared as axioms

Minimal and maximal layers of a set

This file defines Set.minLayer and Set.maxLayer as the sets obtained from iterated application of Minimal/Maximal on a set, excluding earlier layers.

Main declarations

Set.minLayer (Set.maxLayer): the nth minimal (maximal) layer of the given set A.
Set.pairwiseDisjoint_minLayer (Set.pairwiseDisjoint_maxLayer), Set.isAntichain_minLayer (Set.isAntichain_maxLayer): minimal (maximal) layers are pairwise disjoint antichains.
Set.iUnion_minLayer_iff_bounded_series: if the length of LTSeries in A is bounded, A equals the union of its minLayers up to n.

Imports (2)

Imported by 3 files

def Set.minLayer The nth minimal layer of A line 37 source
Source documentation
The nth minimal layer of A.

no axioms what this means
Statement uses: PartialOrder, Set, Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, Set.ofPred, Minimal, Membership.mem, SDiff.sdiff, Set.iUnion
6 instances, coercions and auxiliary constants left out.
```
def minLayer (A : Set α) (n : ℕ) : Set α :=
…
```
Mentions: A
def Set.maxLayer The nth maximal layer of A line 41 source
Source documentation
The nth maximal layer of A.

no axioms what this means
Statement uses: PartialOrder, Set, Nat
Proof uses: Set.minLayer, OrderDual
1 instances, coercions and auxiliary constants left out.
```
def maxLayer (A : Set α) (n : ℕ) : Set α :=
…
```
Mentions: A
def Set.layersAbove The elements above A's n minimal layers line 45 source
Source documentation
The elements above A's n minimal layers.

no axioms what this means
Statement uses: PartialOrder, Set, Nat
Proof uses: SDiff.sdiff, Set.iUnion, LE.le, Set.minLayer
2 instances, coercions and auxiliary constants left out.
```
def layersAbove (A : Set α) (n : ℕ) : Set α :=
…
```
Mentions: A
def Set.layersBelow The elements below A's n maximal layers line 49 source
Source documentation
The elements below A's n maximal layers.

no axioms what this means
Statement uses: PartialOrder, Set, Nat
Proof uses: SDiff.sdiff, Set.iUnion, LE.le, Set.maxLayer
2 instances, coercions and auxiliary constants left out.
```
def layersBelow (A : Set α) (n : ℕ) : Set α :=
…
```
Mentions: A
lemma Set.maxLayer_def line 55 source
standard axioms: Quot.sound what this means
Statement uses: PartialOrder, Set, Nat, Eq, Set.maxLayer, Set.ofPred, Maximal, Membership.mem, SDiff.sdiff, Set.iUnion, LT.lt
Proof uses: Eq.mpr, Set.minLayer, OrderDual, id, congrArg, Set.maxLayer.eq_1, Minimal, Set.minLayer.eq_1, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.minLayer_subset line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, LE.le, Set.minLayer
Proof uses: Trans.trans, SDiff.sdiff, Set.iUnion, LT.lt, Eq.mpr, Set.ofPred, Minimal, Membership.mem, id, Eq, congrArg, Set.minLayer.eq_1, Minimal.prop, Eq.mp, propext, Set.mem_ofPred, Set.sdiff_subset
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Set.maxLayer_subset line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, LE.le, Set.maxLayer
Proof uses: Set.minLayer_subset, OrderDual
2 instances, coercions and auxiliary constants left out.
lemma Set.layersAbove_subset line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, LE.le, Set.layersAbove
Proof uses: Set.sdiff_subset, Set.iUnion, Set.minLayer
2 instances, coercions and auxiliary constants left out.
lemma Set.layersBelow_subset line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, LE.le, Set.layersBelow
Proof uses: Set.sdiff_subset, Set.iUnion, Set.maxLayer
2 instances, coercions and auxiliary constants left out.
lemma Set.minLayer_zero XXX(MR): should this and maxLayer_zero be simp? line 71 source
Source comment
XXX(MR): should this and `maxLayer_zero` be simp?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Eq, Set.minLayer, OfNat.ofNat, Nat, Set.ofPred, Minimal, Membership.mem
Proof uses: Eq.mpr, SDiff.sdiff, Set.iUnion, LT.lt, id, congrArg, Set.minLayer.eq_1, of_eq_true, Eq.trans, True, congrFun', funext, EmptyCollection.emptyCollection, False, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty, Set.sdiff_empty and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma minLayer_zero : A.minLayer 0 = {a | Minimal (· ∈ A) a} := by rw [minLayer]; simp
```
Mentions: A, Set.minLayer
lemma Set.maxLayer_zero line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Eq, Set.maxLayer, OfNat.ofNat, Nat, Set.ofPred, Maximal, Membership.mem
Proof uses: Eq.mpr, SDiff.sdiff, Set.iUnion, LT.lt, id, congrArg, Set.maxLayer_def, of_eq_true, Eq.trans, True, congrFun', funext, EmptyCollection.emptyCollection, False, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty, Set.sdiff_empty and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.disjoint_minLayer_of_ne line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Ne, Disjoint, Set.minLayer
Proof uses: LT.lt, Not, Or, Classical.em, Eq.mpr, Membership.mem, id, Eq, congrArg, propext, Set.disjoint_right, Set.iUnion, And.right, And.left, SDiff.sdiff, LE.le, Eq.mp, Set.ofPred, Minimal, Set.minLayer.eq_1 and 4 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Set.disjoint_maxLayer_of_ne line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Ne, Disjoint, Set.maxLayer
Proof uses: Set.disjoint_minLayer_of_ne, OrderDual
12 instances, coercions and auxiliary constants left out.
lemma Set.pairwiseDisjoint_minLayer line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Set.PairwiseDisjoint, Nat, Set.univ, Set.minLayer
Proof uses: Membership.mem, Set.disjoint_minLayer_of_ne
12 instances, coercions and auxiliary constants left out.
lemma Set.pairwiseDisjoint_maxLayer line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Set.PairwiseDisjoint, Nat, Set.univ, Set.maxLayer
Proof uses: Membership.mem, Set.disjoint_minLayer_of_ne, OrderDual
13 instances, coercions and auxiliary constants left out.
lemma Set.isAntichain_minLayer line 90 source
standard axioms: Quot.sound what this means
Statement uses: PartialOrder, Set, Nat, IsAntichain, LE.le, Set.minLayer
Proof uses: Eq.mpr, Set.ofPred, Minimal, Membership.mem, SDiff.sdiff, Set.iUnion, LT.lt, id, Eq, congrArg, Set.minLayer.eq_1, setOfPred_minimal_antichain
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.isAntichain_maxLayer line 93 source
standard axioms: Quot.sound what this means
Statement uses: PartialOrder, Set, Nat, IsAntichain, LE.le, Set.maxLayer
Proof uses: Eq.mpr, Set.ofPred, Maximal, Membership.mem, SDiff.sdiff, Set.iUnion, LT.lt, id, Eq, congrArg, Set.maxLayer_def, setOfPred_maximal_antichain
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.exists_le_in_minLayer_of_le line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Membership.mem, Set.minLayer, LE.le, Exists, And
Proof uses: Nat.le_induction, Exists.intro, And.intro, le_refl, HAdd.hAdd, OfNat.ofNat, Not, Iff.mp, Disjoint, Set.disjoint_right, Set.disjoint_minLayer_of_ne, SDiff.sdiff, Set.iUnion, LT.lt, And.left, Eq, Eq.mp, Minimal, congrArg, propext and 40 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Set.exists_le_in_maxLayer_of_le line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Membership.mem, Set.maxLayer, LE.le, Exists, And
Proof uses: Set.exists_le_in_minLayer_of_le, OrderDual
7 instances, coercions and auxiliary constants left out.
lemma Set.subtype_mk_minimal_iff XXX: is this in mathlib already/can it also be removed? line 123 source
Source comment
XXX: is this in mathlib already/can it also be removed?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, Set, Membership.mem, Iff, Minimal, Subtype.mk, Exists, And
Proof uses: Subtype, Not, Or, Classical.em, of_eq_true, Eq.trans, Iff.mpr, Iff.of_eq, Eq.refl, True, congr, congrArg, Set.image, OrderEmbedding, RelEmbedding.mk, LE.le, Function.Embedding.subtype, Function.Embedding, forall_congr, congrFun' and 20 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma subtype_mk_minimal_iff (α : Type*) [Preorder α]
    (s : Set α) (t : Set s) (x : α) (hx : x ∈ s) :
    Minimal (· ∈ t) (⟨x, hx⟩ : s) ↔ Minimal (fun y ↦ ∃ h, y ∈ s ∧ ⟨y, h⟩ ∈ t) x := by
…
```
Mentions: s
lemma Set.minLayer_eq_setOf_height A.minLayer n comprises exactly A's elements of height n line 135 source
Source documentation
A.minLayer n comprises exactly A's elements of height n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Eq, Set.minLayer, Set.ofPred, Exists, Membership.mem, ENat, Order.height, Subtype, Subtype.mk
Proof uses: Nat.strongRec, LT.lt, Set.ext, id, Iff, Not, Or, Classical.em, Eq.mpr, Iff.mpr, True, Iff.of_eq, eq_true, True.intro, congrArg, Eq.trans, propext, exists_prop_congr, Eq.refl, Minimal and 46 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma minLayer_eq_setOf_height : A.minLayer n = {x | ∃ hx : x ∈ A, height (⟨x, hx⟩ : A) = n} := by
…
```
Mentions: A
lemma Set.iUnion_lt_minLayer_iff_bounded_series line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Iff, Eq, Set.iUnion, LT.lt, Set.minLayer, LTSeries, Membership.mem, RelSeries.length, Set.ofPred, Prod, FiniteDimensionalOrder.match_1
Proof uses: Iff.intro, RelSeries.last, Eq.rec, Subtype.property, Eq.symm, Exists, ENat, Order.height, Subtype, Prod.fst, Prod.snd, Eq.mp, Subtype.mk, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, Eq.trans, True and 43 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Set.iUnion_minLayer_iff_bounded_series A equals the union of its minLayers up to n iff all LTSeries in A have length at most n line 189 source
Source documentation
A equals the union of its minLayers up to n iff all LTSeries in A have length at most n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Iff, Eq, Set.iUnion, LE.le, Set.minLayer, LTSeries, Membership.mem, RelSeries.length, Set.ofPred, Prod, FiniteDimensionalOrder.match_1, LT.lt
Proof uses: id, Eq.mpr, Prod.fst, Prod.snd, Nat.succ, congr, congrArg, congrFun', funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, forall_congr, of_eq_true, Eq.trans, True, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma iUnion_minLayer_iff_bounded_series :
    ⋃ (k ≤ n), A.minLayer k = A ↔ ∀ p : LTSeries A, p.length ≤ n := by
…
```
Mentions: k, A
lemma Set.exists_le_in_layersAbove_of_le line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Finite, Membership.mem, Set.layersAbove, LE.le, Exists, And, Set.minLayer
Proof uses: SDiff.sdiff, Set.iUnion, LT.lt, Eq.mpr, Not, id, Eq, Eq.trans, congrArg, funext, binderNameHint, forall_congr, And.intro, And.left, Eq.mp, And.right, LT.lt.le, Fintype, Fintype.ofFinite, Finset and 31 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Set.exists_le_in_layersBelow_of_le line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PartialOrder, Set, Nat, Finite, Membership.mem, Set.layersBelow, LE.le, Exists, And, Set.maxLayer
Proof uses: Set.exists_le_in_layersAbove_of_le, OrderDual
8 instances, coercions and auxiliary constants left out.