Compfiles/Imo2011P3.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2011, Problem 3

Let f : ℝ → ℝ be a function that satisfies

f(x + y) ≤ y * f(x) + f(f(x))

for all x and y. Prove that f(x) = 0 for all x ≤ 0.

Imports (3)
Imported by 1 file
  1. problem Imo2011P3.imo2011_p3 line 30 source

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

    Statement uses: Real, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq

    Proof uses: HSub.hSub, Trans.trans, Eq.mpr, id, congrArg, add_eq_of_eq_sub', rfl, Eq.refl, sub_mul, LT.lt, Nat, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance and 93 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

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