Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2011P3


import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith

/-!
# 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.
-/

namespace Imo2011P3

theorem imo2011_p3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f x)) :
    ∀ x ≤ 0, f x = 0 := sorry

This problem has a complete formalized solution written by David Renshaw.

Open with the in-brower editor at live.lean-lang.org:
External resources: