mathlib3 documentation

mathlib-archive / imo.imo1977_q6

IMO 1977 Q6 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Suppose f : ℕ+ → ℕ+ satisfies f(f(n)) < f(n + 1) for all n. Prove that f(n) = n for all n.

We first prove the problem statement for f : ℕ → ℕ then we use it to prove the statement for positive naturals.

theorem imo1977_q6.imo1977_q6_nat (f : ) (h : (n : ), f (f n) < f (n + 1)) (n : ) :
f n = n
theorem imo1977_q6 (f : ℕ+ ℕ+) (h : (n : ℕ+), f (f n) < f (n + 1)) (n : ℕ+) :
f n = n