Continuous angle gap trapped
ProvedBirkhoffGlobalSection.continuous_angle_gap_trappeddynamical-systemstopology
A continuous real function initially strictly between zero and π and never equal to either endpoint stays strictly between those endpoints for all real times.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_contact_winding_width_bundle 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.continuous_angle_gap_trapped :
∀ (g : ℝ → ℝ) (hg : Continuous g)
(h0 : 0 < g 0) (hpi : g 0 < Real.pi)
(hne0 : ∀ t, g t ≠ 0) (hnepi : ∀ t, g t ≠ Real.pi),
∀ t, 0 < g t ∧ g t < Real.pi := by sorrySource
Independent extraction of component 1 of the Proved theorem BirkhoffGlobalSection.contact_winding_width_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_width_bundle.lean. Exact original component retained.