OAI/Analysis/MassAction/FirstExit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.mapsTo_interior_of_initial_segments line 13

   Source documentation

   A continuous curve cannot first leave a closed region if every initial segment inside the region ends in a fixed subset of its interior.

   theorem mapsTo_interior_of_initial_segments {X : Type uX} [TopologicalSpace X]
       {x : ℝ → X} {a b : ℝ} {B K : Set X}
       (hB : IsClosed B) (hK : K ⊆ interior B)
       (hc : ContinuousOn x (Icc a b)) (ha : x a ∈ interior B)
       (htrap : ∀ t ∈ Icc a b, MapsTo x (Icc a t) B → x t ∈ K) :
       MapsTo x (Icc a b) (interior B) := by
   …

2. theorem OAI.Problem326.mapsTo_of_initial_segments line 53

   Source documentation

   Endpoint trapping on every initial segment upgrades to trapping on the entire closed interval once the trapping set lies strictly inside the closed region.

   theorem mapsTo_of_initial_segments {X : Type uX} [TopologicalSpace X]
       {x : ℝ → X} {a b : ℝ} {B K : Set X}
       (hB : IsClosed B) (hK : K ⊆ interior B)
       (hc : ContinuousOn x (Icc a b)) (ha : x a ∈ interior B)
       (htrap : ∀ t ∈ Icc a b, MapsTo x (Icc a t) B → x t ∈ K) :
       MapsTo x (Icc a b) K := by
   …