`Compfiles/Imo1992P5.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 8 curated AI-written annotations and 3305 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 compfiles documentation, Pinned compfiles corpus index

14 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1992, Problem 5

Let S be a finite set of points in three-dimensional space. Let Sx,Sy and Sz be the sets consisting of the orthogonal projections of the points of S onto the yz-plane, zx-plane and xy-plane, respectively. Prove that |S|²≤|Sx|·|Sy|·|Sz|. where |A| denotes the number of elements in the finite set |A|. (Note: The orthogonal projection of a point onto a plane is the foot of the perpendicular from the point to the plane.)

Imports (2)

Imported by 1 file

Compfiles.lean

instance Imo1992P5.(instance at line 31) line 31 source
abbrev Imo1992P5.px Project onto yz-plane (zero out x) line 34 source
Source documentation
Project onto yz-plane (zero out x)
```
private abbrev px (p : ℝ × ℝ × ℝ) : ℝ × ℝ × ℝ := (0, p.2.1, p.2.2)
```
abbrev Imo1992P5.py Project onto xz-plane (zero out y) line 36 source
Source documentation
Project onto xz-plane (zero out y)
```
private abbrev py (p : ℝ × ℝ × ℝ) : ℝ × ℝ × ℝ := (p.1, 0, p.2.2)
```
abbrev Imo1992P5.pz Project onto xy-plane (zero out z) line 38 source
Source documentation
Project onto xy-plane (zero out z)
```
private abbrev pz (p : ℝ × ℝ × ℝ) : ℝ × ℝ × ℝ := (p.1, p.2.1, 0)
```
def Imo1992P5.zslice The slice of S at z-coordinate r line 41 source
Source documentation
The slice of S at z-coordinate r
```
private noncomputable def zslice (S : Finset (ℝ × ℝ × ℝ)) (r : ℝ) :=
…
```
Mentions: S
lemma Imo1992P5.card_sum_slices S is the disjoint union of its z-slices line 45 source
Source documentation
S is the disjoint union of its z-slices
```
private lemma card_sum_slices (S : Finset (ℝ × ℝ × ℝ)) :
    S.card = ∑ r ∈ S.image (·.2.2), (zslice S r).card := by
…
```
Mentions: S, Imo1992P5.zslice
lemma Imo1992P5.slice_le_prod Each z-slice injects into the product of its x- and y-projections line 57 source
Source documentation
Each z-slice injects into the product of its x- and y-projections
```
private lemma slice_le_prod (S : Finset (ℝ × ℝ × ℝ)) (r : ℝ) :
    (zslice S r).card ≤ ((zslice S r).image px).card * ((zslice S r).image py).card := by
…
```
Mentions: S, Imo1992P5.zslice, Imo1992P5.px, Imo1992P5.py
lemma Imo1992P5.slice_le_sz Each z-slice has size ≤ |S_z| (pz is injective on each slice) line 73 source
Source documentation
Each z-slice has size ≤ |S_z| (pz is injective on each slice)
```
private lemma slice_le_sz (S : Finset (ℝ × ℝ × ℝ)) (r : ℝ) :
    (zslice S r).card ≤ (S.image pz).card := by
…
```
Mentions: S, Imo1992P5.zslice, Imo1992P5.pz
lemma Imo1992P5.px_disjoint px-images of different z-slices are disjoint (px preserves z-coordinate) line 86 source
Source documentation
px-images of different z-slices are disjoint (px preserves z-coordinate)
```
private lemma px_disjoint (S : Finset (ℝ × ℝ × ℝ)) {r₁ r₂ : ℝ} (hr : r₁ ≠ r₂) :
    Disjoint ((zslice S r₁).image px) ((zslice S r₂).image px) :=
…
```
Mentions: S, Imo1992P5.zslice, Imo1992P5.px
lemma Imo1992P5.py_disjoint py-images of different z-slices are disjoint line 96 source
Source documentation
py-images of different z-slices are disjoint
```
private lemma py_disjoint (S : Finset (ℝ × ℝ × ℝ)) {r₁ r₂ : ℝ} (hr : r₁ ≠ r₂) :
    Disjoint ((zslice S r₁).image py) ((zslice S r₂).image py) :=
…
```
Mentions: S, Imo1992P5.zslice, Imo1992P5.py
lemma Imo1992P5.sum_px_le Sum of |px-image of slice| ≤ |Sx| line 106 source
Source documentation
Sum of |px-image of slice| ≤ |Sx|
```
private lemma sum_px_le (S : Finset (ℝ × ℝ × ℝ)) :
    ∑ r ∈ S.image (·.2.2), ((zslice S r).image px).card ≤ (S.image px).card := by
…
```
Mentions: S, Imo1992P5.zslice, Imo1992P5.px
lemma Imo1992P5.sum_py_le Sum of |py-image of slice| ≤ |Sy| line 113 source
Source documentation
Sum of |py-image of slice| ≤ |Sy|
```
private lemma sum_py_le (S : Finset (ℝ × ℝ × ℝ)) :
    ∑ r ∈ S.image (·.2.2), ((zslice S r).image py).card ≤ (S.image py).card := by
…
```
Mentions: S, Imo1992P5.zslice, Imo1992P5.py
theorem Imo1992P5.main Main inequality: |S|² ≤ |Sx| · |Sy| · |Sz| line 120 source
Source documentation
Main inequality: |S|² ≤ |Sx| · |Sy| · |Sz|
```
private theorem main (S : Finset (ℝ × ℝ × ℝ)) :
    (S.card : ℝ) ^ 2 ≤ (S.image px).card * (S.image py).card * (S.image pz).card := by
…
```
Mentions: S, Imo1992P5.px, Imo1992P5.py, Imo1992P5.pz
problem Imo1992P5.imo1992_p5 line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Real, LE.le, Nat, HPow.hPow, Finset.card, OfNat.ofNat, HMul.hMul, Finset.image, Prod.mk, Prod.fst, Prod.snd
Proof uses: cast, Eq.trans, congr, congrArg, congrFun', Eq.symm, funext, Nat.cast_zero
57 instances, coercions and auxiliary constants left out.

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