Compfiles/Imo2022P2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2022, Problem 2

Let ℝ+ be the set of positive real numbers. Determine all functions f: ℝ+ → ℝ+ such that for each x ∈ ℝ+, there is exactly one y ∈ ℝ+ satisfying

x·f(y) + y·f(x) ≤ 2

Imports (4)
Imported by 1 file
  1. abbrev Imo2022P2.PosReal line 32 source

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

    Proof uses: Subtype, Real, LT.lt, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. lemma Imo2022P2.lemma0 line 38 source

    standard axioms: Classical.choice what this means

    Statement uses: ExistsUnique, Iff, Eq, Classical.choose, ExistsUnique.exists

    Proof uses: And, Exists.intro, Eq.mpr, And.intro, id, congrArg, Classical.choose_spec, Iff.mpr

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  3. lemma Imo2022P2.amgm line 48 source

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

    Statement uses: Imo2022P2.PosReal, LE.le, Real, LT.lt, OfNat.ofNat, Subtype.mk, Nat, two_pos, HAdd.hAdd, HDiv.hDiv

    Proof uses: id, of_eq_true, Eq.trans, HMul.hMul, inferInstance, CommGroupWithZero, HPow.hPow, GroupWithZero, True, Mathlib.Tactic.FieldSimp.le_eq_cancel_le, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.refl and 38 more

    141 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  4. lemma Imo2022P2.lemma1 line 54 source

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

    Statement uses: Imo2022P2.PosReal, Eq, HAdd.hAdd, Real, HMul.hMul, Subtype.mk, LT.lt, OfNat.ofNat, Nat, two_pos

    Proof uses: Subtype.val_injective, Eq.symm, two_mul

    85 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. determine Imo2022P2.solution_set line 61 source

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

    Statement uses: Set, Imo2022P2.PosReal

    Proof uses: Singleton.singleton, HDiv.hDiv, Real, OfNat.ofNat

    13 instances, coercions and auxiliary constants left out.

  6. problem Imo2022P2.imo2022_p2 line 63 source

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

    Statement uses: Imo2022P2.PosReal, Iff, Membership.mem, Set, Imo2022P2.solution_set, ExistsUnique, LE.le, Real, LT.lt, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Subtype.mk, Nat, two_pos

    Proof uses: Iff.intro, Eq.mpr, HDiv.hDiv, id, Eq, congrArg, Eq.mp, Exists.intro, And, And.intro, of_eq_true, Subtype, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congr, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat and 156 more

    220 instances, coercions and auxiliary constants left out.

    Tactic trace: 104 steps

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