Compfiles/Imo1986P5.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1986, Problem 5

Find all functions f, defined on the non-negative real numbers and taking nonnegative real values, such that:

Imports (2)
Imported by 1 file
  1. structure Imo1986P5.IsGood line 35 source

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

    Statement uses: NNReal

  2. theorem Imo1986P5.IsGood.map_add line 55 source

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

    Statement uses: NNReal, Imo1986P5.IsGood, Eq, HAdd.hAdd, HMul.hMul

    Proof uses: Eq.symm, Imo1986P5.IsGood.map_add_rev

    12 instances, coercions and auxiliary constants left out.

  3. theorem Imo1986P5.IsGood.map_eq_zero line 58 source

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

    Statement uses: NNReal, Imo1986P5.IsGood, Iff, Eq, OfNat.ofNat, LE.le, Nat

    Proof uses: Iff.intro, Iff.mp, Not, LT.lt, not_lt, Imo1986P5.IsGood.map_ne_zero, HAdd.hAdd, Exists, ExistsAddOfLE.exists_add_of_le, Eq.mpr, id, congrArg, add_comm, HMul.hMul, Imo1986P5.IsGood.map_add, Imo1986P5.IsGood.map_two, MulZeroClass.mul_zero, Eq.refl, Eq.symm

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  4. theorem Imo1986P5.IsGood.map_ne_zero_iff line 63 source

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

    Statement uses: NNReal, Imo1986P5.IsGood, Iff, Ne, OfNat.ofNat, LT.lt, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Not, Eq, LE.le, propext, Imo1986P5.IsGood.map_eq_zero, iff_self

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem Imo1986P5.IsGood.map_of_lt_two line 65 source

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

    Statement uses: NNReal, Imo1986P5.IsGood, LT.lt, OfNat.ofNat, Nat, Eq, HDiv.hDiv, HSub.hSub

    Proof uses: tsub_pos_of_lt, Ne, Iff.mpr, Imo1986P5.IsGood.map_ne_zero_iff, le_antisymm, Eq.mpr, LE.le, HMul.hMul, id, congrArg, propext, le_div_iff₀, Eq.symm, le_div_iff₀', Ne.bot_lt, HAdd.hAdd, tsub_le_iff_right, Imo1986P5.IsGood.map_eq_zero, Imo1986P5.IsGood.map_add, div_mul_cancel₀ and 12 more

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  6. theorem Imo1986P5.IsGood.map_eq line 76 source

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

    Statement uses: NNReal, Imo1986P5.IsGood, Eq, HDiv.hDiv, OfNat.ofNat, Nat, HSub.hSub

    Proof uses: Or, LT.lt, LE.le, lt_or_ge, Imo1986P5.IsGood.map_of_lt_two, Eq.mpr, id, congrArg, tsub_eq_zero_of_le, div_zero, propext, Imo1986P5.IsGood.map_eq_zero

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. determine Imo1986P5.SolutionSet line 84 source

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

    Statement uses: Set, NNReal

    Proof uses: Singleton.singleton, HDiv.hDiv, OfNat.ofNat, HSub.hSub

    12 instances, coercions and auxiliary constants left out.

  8. problem Imo1986P5.imo1986_p5 line 86 source

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

    Statement uses: NNReal, Iff, Imo1986P5.IsGood, Membership.mem, Set, Imo1986P5.SolutionSet

    Proof uses: Iff.intro, funext, HDiv.hDiv, OfNat.ofNat, HSub.hSub, Imo1986P5.IsGood.map_eq, Imo1986P5.IsGood.mk, LT.lt, Nat, LE.le, Or, Eq, lt_or_ge, HMul.hMul, HAdd.hAdd, Or.inl, Ne, LT.lt.ne', tsub_pos_of_lt, Eq.mpr and 31 more

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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