FormalConjectures/ErdosProblems/139.lean

GitHub source file

2 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 139

Reference: erdosproblems.com/139

Imports (1)
  1. abbrev Erdos139.r line 33 source

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

    Statement uses: Nat

    Proof uses: Set.IsAPOfLengthFree.maxCard

  2. theorem Erdos139.erdos_139 sorry line 42 source

    depends on sorry what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Filter.Tendsto, Real, HDiv.hDiv, Erdos139.r, Filter.atTop, nhds

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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