Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1992P5

import Mathlib

/-!
# 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.)
-/

namespace Imo1992P5

theorem imo1992_p5 (S: Finset (ℝ × ℝ × ℝ)) : S.card^2 ≤
    (Finset.image (fun p => ((0: ℝ) , p.2.1, p.2.2)) S).card *
    (Finset.image (fun p => (p.1, ((0: ℝ) , p.2.2))) S).card *
    (Finset.image (fun p => (p.1, p.2.1, (0: ℝ) )) S).card := sorry


end Imo1992P5

File author(s): Sebastian Willmann (with assistance from Github Copilot and Aristotle)

This problem has a complete formalized solution.