Compfiles/Imo1983P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1983, Problem 1

Let ℝ+ be the set of positive real numbers.

Determine all functions f : ℝ+ → ℝ+ which satisfy: i) f(xf(y)) = yf(x) for all x y ∈ ℝ+. ii) f(x) → 0 as x → ∞.

Imports (3)
Imported by 1 file
  1. abbrev Imo1983P1.PosReal line 30 source

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

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

    3 instances, coercions and auxiliary constants left out.

  2. determine Imo1983P1.SolutionSet line 34 source

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

    Statement uses: Set, Imo1983P1.PosReal

    Proof uses: Singleton.singleton, HDiv.hDiv, Real, OfNat.ofNat

    13 instances, coercions and auxiliary constants left out.

  3. problem Imo1983P1.imo1983_p1 line 36 source

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

    Statement uses: Imo1983P1.PosReal, Iff, Membership.mem, Set, Imo1983P1.SolutionSet, And, Eq, HMul.hMul, Real, Exists, LT.lt, OfNat.ofNat

    Proof uses: Iff.intro, HDiv.hDiv, And.intro, of_eq_true, Eq.trans, Inv.inv, True, congr, congrArg, one_div, mul_inv_rev, congrFun', inv_inv, eq_self, Exists.intro, id, Iff.mp, div_lt_comm, Eq.symm, Eq.mpr and 102 more

    177 instances, coercions and auxiliary constants left out.

    Tactic trace: 86 steps

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