FormalConjectures/ErdosProblems/899.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 899

Reference: erdosproblems.com/899

Imports (1)
  1. theorem Erdos899.erdos_899 sorry line 49 source

    depends on sorry what this means

    Statement uses: Iff, True, Set, Nat, Set.Infinite, Filter.Tendsto, Real, HDiv.hDiv, Set.ncard, Inter.inter, Set.Icc, OfNat.ofNat, Filter.atTop, nhds, Eq, EReal, Filter.limsup, HSub.hSub, Top.top

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

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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