Compfiles/Imo1994P5.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1994, Problem 5

Let S be the set of all real numbers greater than -1. Find all functions f : S→S such that f(x + f(y) + xf(y)) = y + f(x) + yf(x) for all x and y, and f(x)/x is strictly increasing on each of the intervals -1 < x < 0 and 0 < x.

Imports (2)
Imported by 1 file
  1. def Imo1994P5.S line 28 source

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

    Proof uses: Subtype, Real, LT.lt, Neg.neg, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

  2. abbrev Imo1994P5.op line 30 source

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

    Statement uses: Imo1994P5.S

    Proof uses: Subtype.mk, Real, LT.lt, Neg.neg, OfNat.ofNat, HAdd.hAdd, HMul.hMul

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Imo1994P5.sol_prop line 35 source

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

    Statement uses: Real, LT.lt, Neg.neg, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd

    Proof uses: Iff.mpr, HMul.hMul, lt_div_iff₀, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.neg_congr and 40 more

    110 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. determine Imo1994P5.solution_set line 40 source

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

    Statement uses: Set, Imo1994P5.S

    Proof uses: Singleton.singleton, Subtype.mk, Real, LT.lt, Neg.neg, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd

    12 instances, coercions and auxiliary constants left out.

  5. problem Imo1994P5.imo1994_p5 line 42 source

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

    Statement uses: Imo1994P5.S, Iff, Membership.mem, Set, Imo1994P5.solution_set, And, Eq, Imo1994P5.op, Real, Set.Ioo, Neg.neg, OfNat.ofNat, LT.lt, HDiv.hDiv

    Proof uses: Iff.intro, Eq.mpr, Subtype.mk, HAdd.hAdd, id, congrArg, Set.eq_of_mem_singleton, And.intro, Eq.trans, implies_congr, Eq.refl, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 140 more

    161 instances, coercions and auxiliary constants left out.

    Tactic trace: 112 steps

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