FormalConjectures/ErdosProblems/421.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 421

References:

Imports (1)
  1. theorem Erdos421.erdos_421 sorry line 39 source

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Nat, And, StrictMono, LE.le, OfNat.ofNat, Set.HasDensity, Set.range, Real, Set.univ, Set.InjOn, Prod, Erdos421.erdos_421.match_1, Finset.prod, Finset.Icc, Set.ofPred

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

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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