Compfiles/Usa2023P2.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

6 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2023, Problem 2

Let ℝ+ be the set of positive real numbers. Find all functions f: ℝ+ → ℝ+ that satisfy the equation

f(x⬝y + f(x)) = x⬝f(y) + 2

for all x,y ∈ ℝ+.

Imports (4)
Imported by 1 file
  1. abbrev Usa2023P2.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 Usa2023P2.val_div Should this be in mathlib as Positive.val_div? line 39 source

    Source comment

    Should this be in mathlib as `Positive.val_div`?

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

    Statement uses: Usa2023P2.PosReal, Eq, Real, LT.lt, OfNat.ofNat, HDiv.hDiv

    Proof uses: Eq.refl

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    lemma val_div (a b : ℝ+) : (a / b).val = a.val / b.val := by rfl
  3. lemma Usa2023P2.lemma_1 line 41 source

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

    Statement uses: Usa2023P2.PosReal, Eq, HDiv.hDiv, Real, HAdd.hAdd

    Proof uses: Eq.mpr, HMul.hMul, Inv.inv, id, congrArg, division_def, add_mul, Eq.symm, Eq.refl

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma Usa2023P2.lemma_3 line 44 source

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

    Statement uses: Usa2023P2.PosReal, Eq, HAdd.hAdd, Real, LT.lt, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, Subtype, Eq.symm, propext, Subtype.coe_lt_coe, Positive.coe_add, lt_add_of_pos_left, Subtype.property

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  5. determine Usa2023P2.solution_set line 50 source

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

    Statement uses: Set, Usa2023P2.PosReal

    Proof uses: Singleton.singleton, HAdd.hAdd, Real, OfNat.ofNat

    11 instances, coercions and auxiliary constants left out.

  6. problem Usa2023P2.usa2023_p2 line 52 source

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

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

    Proof uses: Iff.intro, Eq.mpr, id, congrArg, Eq.mp, Singleton.singleton, propext, Set.mem_singleton_iff, Usa2023P2.solution_set.eq_1, mul_add, Eq.symm, add_assoc, mul_one, HAdd, Eq.rec, Eq.refl, Subtype, Subtype.property, Subtype.mk_eq_mk, of_eq_true and 148 more

    222 instances, coercions and auxiliary constants left out.

    Tactic trace: 123 steps

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