OAI/NumberTheory/EgyptianFractions/EgyptianExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.exists_strict_unit_fraction_sum line 9

   Source documentation

   Elementary greedy existence, stated independently of the shared definitions.

   theorem exists_strict_unit_fraction_sum (a b : ℕ) (ha : 1 ≤ a) (hab : a < b) :
       ∃ k : ℕ, ∃ n : Fin k → ℕ,
         (∀ i, 2 ≤ n i) ∧ StrictMono n ∧
         (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) = (a : ℚ) / (b : ℚ) := by
   …