Prove2Me

Winding image strict lower bound iff

Proved
BirkhoffGlobalSection.winding_image_strict_lower_bound_iff

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemstopology

When a function's image over [0,2π] is exactly a nonempty closed interval [a,b], all of those values exceed a threshold c exactly when a exceeds c.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_winding_interval_bundle

open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology

set_option maxHeartbeats 800000
open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.winding_image_strict_lower_bound_iff :
∀ (d : ℝ → ℝ) (a b c : ℝ)
    (hab : a ≤ b) (himage : d '' Icc 0 (2 * Real.pi) = Icc a b),
    (∀ s ∈ Icc 0 (2 * Real.pi), c < d s) ↔ c < a := by sorry
Source
Independent extraction of component 6 of the Proved theorem BirkhoffGlobalSection.contact_winding_interval_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_interval_bundle.lean. Exact original component retained.

View graph