Compfiles/Imo2002P5.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2002, Problem 5

Determine all functions f : ℝ → ℝ such that

(f(x) + f(z))(f(y) + f(t)) = f(xy - zt) + f(xt + yz)

for all real numbers x,y,z,t.

Imports (2)
Imported by 1 file
  1. lemma Imo2002P5.extend_function_mono line 31 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, Continuous, Rat, Eq, LT.lt

    Proof uses: Decidable.byContradiction, Not, abs, HSub.hSub, Iff.mpr, Ne, abs_sub_pos, And, GT.gt, Dist.dist, Exists, False, Iff.mp, Metric.continuous_iff, Or, lt_trichotomy, le_or_gt, exists_rat_btwn, Exists.intro, And.intro and 74 more

    109 instances, coercions and auxiliary constants left out.

    Tactic trace: 71 steps

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

  2. determine Imo2002P5.SolutionSet line 107 source

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

    Statement uses: Set, Real

    Proof uses: Insert.insert, OfNat.ofNat, HDiv.hDiv, Singleton.singleton, HPow.hPow, Nat

    17 instances, coercions and auxiliary constants left out.

  3. problem Imo2002P5.imo2002_p5 line 110 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo2002P5.SolutionSet, Eq, HMul.hMul, HAdd.hAdd, HSub.hSub

    Proof uses: Eq.mpr, Or, OfNat.ofNat, Inv.inv, HPow.hPow, Nat, id, congrFun', congrArg, Eq.trans, Insert.insert, HDiv.hDiv, Singleton.singleton, funext, one_div, Iff.intro, of_eq_true, True, congr, add_zero and 225 more

    213 instances, coercions and auxiliary constants left out.

    Tactic trace: 158 steps

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