PlateauGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Geometry.subset_interior_of_disjoint_frontier line 13
Source documentation
Boundary exclusion traps any preconnected set that meets the interior. This is the purely topological step in the plateau-polytope construction.
```
theorem subset_interior_of_disjoint_frontier
    {X : Type uX} [TopologicalSpace X] {K B : Set X}
    (hK : IsPreconnected K) (hmeet : (K ∩ interior B).Nonempty)
    (hboundary : Disjoint K (frontier B)) : K ⊆ interior B := by
…
```

theorem OAI.Problem326.Geometry.isCompact_of_disjoint_frontier line 26

Source documentation

A closed preconnected plateau that meets the interior of a compact box and misses its boundary is compact. No boundedness assumption on the ambient compatibility class is needed.

theorem isCompact_of_disjoint_frontier
    {X : Type uX} [TopologicalSpace X] {K B : Set X}
    (hKclosed : IsClosed K) (hKconn : IsPreconnected K)
    (hBcompact : IsCompact B) (hmeet : (K ∩ interior B).Nonempty)
    (hboundary : Disjoint K (frontier B)) : IsCompact K := by
…

theorem OAI.Problem326.Geometry.mapsTo_interior_of_no_first_boundary line 40

Source documentation

A continuous curve cannot leave an interior if each segment in the closed ambient set is forbidden from ending on its boundary.

theorem mapsTo_interior_of_no_first_boundary
    {X : Type uX} [TopologicalSpace X] {B : Set X} {T : ℝ}
    {x : ℝ → X} (hT : 0 ≤ T) (hB : IsClosed B)
    (hx : ContinuousOn x (Set.Icc 0 T)) (hx0 : x 0 ∈ interior B)
    (hblock : ∀ τ ∈ Set.Icc 0 T,
      Set.MapsTo x (Set.Icc 0 τ) B → x τ ∉ frontier B) :
    Set.MapsTo x (Set.Icc 0 T) (interior B) := by
…

theorem OAI.Problem326.Geometry.mapsTo_plateau_of_monotone_on_box line 88

Source documentation

Monotonicity inside a box, together with a global ceiling and exclusion of boundary maximizers, confines a whole continuous segment to its plateau.

theorem mapsTo_plateau_of_monotone_on_box
    {X : Type uX} [TopologicalSpace X] {B : Set X} {T M : ℝ}
    {x : ℝ → X} {F : X → ℝ} (hT : 0 ≤ T) (hB : IsClosed B)
    (hx : ContinuousOn x (Set.Icc 0 T)) (hx0 : x 0 ∈ interior B)
    (hFM : ∀ z, F z ≤ M) (hF0 : F (x 0) = M)
    (hboundary : ∀ z ∈ frontier B, F z ≠ M)
    (hmono : ∀ τ ∈ Set.Icc 0 T, Set.MapsTo x (Set.Icc 0 τ) B →
      MonotoneOn (F ∘ x) (Set.Icc 0 τ)) :
    Set.MapsTo x (Set.Icc 0 T) {z | z ∈ interior B ∧ F z = M} := by
…