Riesz's rising sun lemma

rising_sun_lemma

Submitter: Kim Morrison.

Notes: Every continuous real function on a compact interval has the rising-sun property: the shadow set is open, empty iff the function is antitone, else a disjoint union of open intervals with f(c_n) ≤ f(d_n). Trusted helpers (risingSunSet, HasRisingSunDecomposition, HasRisingSunProperty) are non-holes. Mathlib has the monotone-a.e.-differentiable consequence but not the rising-sun lemma. Candidate from §163 of the Knill survey.

Source: F. Riesz (1932). Knill, §163.

Informal solution: Unavailable.

theorem declaration uses `sorry`rising_sun_lemma {a b : ℝ} (hab : a < b) {f : ℝ → ℝ}
    (hf : ContinuousOn f (Icc a b)) :
    LeanEval.Analysis.RisingSun.HasRisingSunProperty a b f := bya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Icc a b)⊢ HasRisingSunProperty a b f
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026