Formal target: Corpus.Erdos282.erdos_282

Let $A\subseteq \mathbb{N}$ be an infinite set and consider the following greedy algorithm for a rational $x\in (0,1)$: choose the minimal $n\in A$ such that $n\geq 1/x$ and repeat with $x$ replaced by $x-\frac{1}{n}$.

Exact formal statement

∀ {x : Rat},
  Membership.mem.{0, 0} (Set.Ioo.{0} 0 1) x →
    Odd.{0} x.den →
      Filter.EventuallyEq.{0, 0} Filter.atTop.{0}
        (Corpus.Erdos282.greedyUnitFractionRem (Set.ofPred.{0} fun n => Odd.{0} n) x) 0

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record