Compfiles/Imo1992P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1992, Problem 2

Determine all functions f : ℝ → ℝ such that for all x,y ∈ ℝ, f(x² + f(y)) = y + (f(x))².

Imports (2)
Imported by 1 file
  1. determine Imo1992P2.solution_set line 26 source

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

    Statement uses: Set, Real

    Proof uses: Singleton.singleton

    1 instances, coercions and auxiliary constants left out.

  2. problem Imo1992P2.imo1992_p2 line 28 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo1992P2.solution_set, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, Singleton.singleton, propext, Set.mem_singleton_iff, Iff.intro, congr, Lean.Data.AC.Context.eq_of_norm, Lean.Data.AC.Context.mk, Option.some, PLift, Std.Commutative, PLift.up, Option.none, Std.IdempotentOp, List.cons, Lean.Data.AC.Variable, Lean.Data.AC.Variable.mk, Std.LawfulIdentity and 133 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 89 steps

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