Compfiles/Usa1983P3.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

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1983, Problem 3

S₁, S₂, ..., Sₙ are subsets of the real line. Each Sᵢ is the union of two closed intervals. Any three Sᵢ have a point in common. Show that there is a point which belongs to at least half the Sᵢ.

Imports (5)
Imported by 1 file
  1. lemma Usa1983P3.mem_leftMax_or_rightMin Documented declaration: mem_leftMax_or_rightMin line 36 source

    Source documentation

    Key covering step of the solution: writing each set of the family as Icc (a i) (b i) ∪ Icc (c i) (d i), every set contains either a h, where h maximizes the left endpoint a, or d k, where k minimizes the right endpoint d. Otherwise a common point of S i, S h and S k would have to lie left of a h inside S h, or right of d k inside S k.

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

    Statement uses: Nat, Fin, Set, Real, LE.le, Eq, Union.union, Set.Icc, Set.Nonempty, Inter.inter, Or, Membership.mem

    Proof uses: Classical.byContradiction, Not, And, False, Eq.mp, LT.lt, Eq.mpr, id, congrArg, Set.mem_union_left, lt_of_not_ge, propext, not_and, Set.mem_Icc, Set.mem_union_right, not_and', And.left, Iff.mp, LE.le.trans, And.right and 4 more

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 40 steps

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

    lemma mem_leftMax_or_rightMin {n : ℕ} {S : Fin n → Set ℝ}
    {a b c d : Fin n → ℝ} (hab : ∀ i, a i ≤ b i) (hbc : ∀ i, b i ≤ c i)
    (hcd : ∀ i, c i ≤ d i)
    (hSd : ∀ i, S i = Set.Icc (a i) (b i) ∪ Set.Icc (c i) (d i))
    {h k : Fin n} (hmax : ∀ i, a i ≤ a h) (hmin : ∀ i, d k ≤ d i)
    (h3 : ∀ i j k : Fin n, (S i ∩ S j ∩ S k).Nonempty) (i : Fin n) :
    a h ∈ S i ∨ d k ∈ S i := by
…

    Mentions: S, h

  2. problem Usa1983P3.usa1983_p3 line 84 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Set, Real, Exists, And, LE.le, Eq, Union.union, Set.Icc, Set.Nonempty, Inter.inter, HMul.hMul, Set.ncard, Set.ofPred, Membership.mem

    Proof uses: Nonempty, Nonempty.intro, Fin.mk, Finset, Finset.univ, Finset.exists_max_image, Finset.univ_nonempty, Finset.exists_min_image, Finset.mem_univ, Or, Usa1983P3.mem_leftMax_or_rightMin, And.left, And.right, Set.univ, HAdd.hAdd, Set.ncard_le_ncard, Set.toFinite, LE.le.trans, Eq.mp, Fintype.card and 10 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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