Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1987P3

module

public import Mathlib.Algebra.Polynomial.Eval.Defs
public import Mathlib.Data.Real.Basic

public section


/-!
# USA Mathematical Olympiad 1987, Problem 3

X is the smallest set of polynomials p(x) such that:
(1) p(x) = x belongs to X; and
(2) if r(x) belongs to X, then x·r(x) and (x + (1 - x)·r(x)) both belong to X.

Show that if r(x) and s(x) are distinct elements of X, then r(x) ≠ s(x)
for any 0 < x < 1.
-/

namespace Usa1987P3

open Polynomial

theorem usa1987_p3
    (S : Set (Polynomial ℝ))
    (hX : Polynomial.X ∈ S)
    (hmul : ∀ r ∈ S, Polynomial.X * r ∈ S)
    (hcomb : ∀ r ∈ S, Polynomial.X + (1 - Polynomial.X) * r ∈ S)
    (hmin : ∀ T : Set (Polynomial ℝ), Polynomial.X ∈ T →
        (∀ r ∈ T, Polynomial.X * r ∈ T) →
        (∀ r ∈ T, Polynomial.X + (1 - Polynomial.X) * r ∈ T) → S ⊆ T)
    {r s : Polynomial ℝ} (hr : r ∈ S) (hs : s ∈ S) (hne : r ≠ s)
    {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) :
    r.eval x ≠ s.eval x := sorry

end Usa1987P3

File author(s): Kimi K3

This problem has a complete formalized solution.