Compfiles/Imo2010P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2010, Problem 1

Determine all functions f : ℝ → ℝ such that for all x,y ∈ ℝ,

f(⌊x⌋y) = f(x)⌊f(y)⌋.

Imports (2)
Imported by 1 file
  1. determine Imo2010P1.solution_set line 31 source

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

    Statement uses: Set, Real

    Proof uses: Set.ofPred, Or, Exists, And, Eq, Int, Int.floor, OfNat.ofNat, Function.const

    6 instances, coercions and auxiliary constants left out.

  2. problem Imo2010P1.imo2010_p1 line 34 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo2010P1.solution_set, Eq, HMul.hMul, Int.floor

    Proof uses: Iff.intro, Or.elim, Exists, And, Int, OfNat.ofNat, Function.const, Exists.elim, Eq.rec, Eq.symm, mul_one, Int.cast_one, And.left, And.right, MulZeroClass.zero_mul, Or.imp, Exists.intro, And.intro, Iff.mp, Int.cast_eq_one and 30 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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