IMO 2013 Q5 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
ℚ>₀ be the positive rational numbers. Let
f : ℚ>₀ → ℝ be a function satisfying
f(x) * f(y) ≥ f(x * y)
f(x + y) ≥ f(x) + f(y)
x, y ∈ ℚ>₀. Given that
f(a) = a for some rational
a > 1, prove that
f(x) = x for
x ∈ ℚ>₀.
We provide a direct translation of the solution found in
Like le_of_all_pow_lt_succ, but with a weaker assumption for y.