Compfiles/Imo1973P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

Imports (2)
Imported by 1 file
  1. problem Imo1973P5.imo1973_p5 line 30 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set, Real, Membership.mem, Exists, And, Ne, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, Function.comp, Function.invFun

    Proof uses: dite, Set.Nonempty, Classical.propDecidable, id, Exists.intro, Eq.mpr, congrArg, Function.Injective, Or, implies_congr, Eq.trans, Eq.refl, False.elim, HSub.hSub, HDiv.hDiv, inferInstance, CommGroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil and 95 more

    128 instances, coercions and auxiliary constants left out.

    Tactic trace: 94 steps

    Open to load the checked before-and-after goal states.