Compfiles/Romania1998P12.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Romanian Mathematical Olympiad 1998, Problem 12

Find all functions u : ℝ → ℝ for which there exists a strictly monotonic function f : ℝ → ℝ such that

∀ x,y ∈ ℝ, f(x + y) = f(x)u(y) + f(y)

Imports (4)
Imported by 1 file
  1. lemma Romania1998P12.extend_function_mono line 38 source

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

    Statement uses: Real, Monotone, Continuous, Rat, Eq

    Proof uses: Classical.byContradiction, Not, Ne, Exists, False, Eq.mp, Mathlib.Tactic.Push.not_forall_eq, abs, HSub.hSub, LT.lt, OfNat.ofNat, Iff.mpr, abs_sub_pos, And, GT.gt, Dist.dist, Iff.mp, Metric.continuous_iff, Or, lt_trichotomy and 73 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 60 steps

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

  2. lemma Romania1998P12.extend_function_anti line 110 source

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

    Statement uses: Real, Antitone, Continuous, Rat, Eq

    Proof uses: Classical.byContradiction, Not, Ne, Exists, False, Eq.mp, Mathlib.Tactic.Push.not_forall_eq, abs, HSub.hSub, LT.lt, OfNat.ofNat, Iff.mpr, abs_sub_pos, And, GT.gt, Dist.dist, Iff.mp, Metric.continuous_iff, Or, lt_trichotomy and 77 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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

  3. lemma Romania1998P12.int_dichotomy line 182 source

    standard axioms: propext what this means

    Statement uses: Int, Exists, Nat, Or, Eq, Neg.neg

    Proof uses: Int.ofNat, Exists.intro, Or.inl, of_eq_true, eq_self, Eq.symm, Int.negSucc, HAdd.hAdd, OfNat.ofNat, Or.inr, Eq.refl

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  4. lemma Romania1998P12.exp_characterization line 187 source

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

    Statement uses: Real, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Or, StrictMono, StrictAnti, Exists, Real.exp

    Proof uses: Nat, HPow.hPow, Nat.recAux, Eq.mpr, id, congrFun', congrArg, Eq.trans, CharP.cast_eq_zero, MulZeroClass.zero_mul, Nat.succ, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul and 179 more

    197 instances, coercions and auxiliary constants left out.

    Tactic trace: 119 steps

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

  5. lemma Romania1998P12.exp_strict_mono' line 312 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Real.exp, HMul.hMul

    Proof uses: Iff.mpr, Real.exp_lt_exp, mul_lt_mul_iff_right₀

    22 instances, coercions and auxiliary constants left out.

  6. lemma Romania1998P12.exp_strict_anti' line 316 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Real.exp, HMul.hMul

    Proof uses: Iff.mpr, Real.exp_lt_exp, mul_lt_mul_of_neg_left, HAdd.hAdd, Function.swap

    37 instances, coercions and auxiliary constants left out.

  7. lemma Romania1998P12.romania1998_p12_mp line 320 source

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

    Statement uses: Real, Exists, And, Or, StrictMono, StrictAnti, Eq, HAdd.hAdd, HMul.hMul, Real.exp

    Proof uses: OfNat.ofNat, Eq.mp, congrArg, add_zero, Ne, HDiv.hDiv, HSub.hSub, Trans.trans, Eq.symm, sub_eq_of_eq_add', Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf and 135 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 138 steps

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

  8. lemma Romania1998P12.romania1998_p12_mpr line 455 source

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

    Statement uses: Real, Exists, Eq, Real.exp, HMul.hMul, And, Or, StrictMono, StrictAnti, HAdd.hAdd

    Proof uses: OfNat.ofNat, Ne, eq_or_ne, Exists.intro, id, And.intro, Or.inl, strictMono_id, Eq.mpr, congrArg, MulZeroClass.zero_mul, Real.exp_zero, mul_one, id_def, Eq.refl, Eq.symm, HSub.hSub, dite, LT.lt, Romania1998P12.exp_strict_mono' and 54 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 36 steps

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

  9. determine Romania1998P12.solution_set line 494 source

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

    Statement uses: Set, Real

    Proof uses: Set.ofPred, Exists, Eq, Real.exp, HMul.hMul

    2 instances, coercions and auxiliary constants left out.

  10. problem Romania1998P12.romania1998_p12 line 497 source

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

    Statement uses: Real, Iff, Exists, And, Or, StrictMono, StrictAnti, Eq, HAdd.hAdd, HMul.hMul, Membership.mem, Set, Romania1998P12.solution_set

    Proof uses: Iff.intro, Romania1998P12.romania1998_p12_mp, Romania1998P12.romania1998_p12_mpr

    12 instances, coercions and auxiliary constants left out.