Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1973P5

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1973, Problem 5

$G$ is a set of non-constant functions of the real variable $x$ of the form
\[f(x) = ax + b, a \text{ and } b \text{ are real numbers,}\] and $G$ has the following properties:
(a) If $f$ and $g$ are in $G$, then $g \circ f$ is in $G$; here $(g \circ f)(x) = g[f(x)]$.
(b) If $f$ is in $G$, then its inverse $f^{-1}$ is in $G$;
    here the inverse of $f(x) = ax + b$ is $f^{-1}(x) = (x - b) / a$.
(c) For every $f$ in $G$, there exists a real number $x_f$ such that $f(x_f) = x_f$.
Prove that there exists a real number $k$ such that $f(k) = k$ for all $f$ in $G$.
-/

namespace Imo1973P5

theorem imo1973_p5 {G : Set (ℝ → ℝ)}
    (hf: ∀ f ∈ G, ∃ a b : ℝ, a ≠ 0 ∧ ∀ x : ℝ, f x = a * x + b)
    (hG : ∀ f ∈ G, ∀ g ∈ G, g ∘ f ∈ G)
    (hinv : ∀ f ∈ G, (∀ x, f x ≠ 0) → f⁻¹ ∈ G)
    (hfix : ∀ f ∈ G, ∃ x, f x = x) :
    ∃ k : ℝ, ∀ f ∈ G, f k = k := sorry


end Imo1973P5

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.