OAI/Geometry/SurfaceImmersion/Whitney/CompactCollarPositivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strict inequalities on a compact curve set propagate to a collar, uniformly in a compact angular parameter.

  1. theorem OAI.ClosedSurfaceR4.CollarVelocity.compact_collar_positive line 16
  2. theorem OAI.ClosedSurfaceR4.CollarVelocity.compact_collar_positive_small_shift line 42

    Source documentation

    The collar and allowed translation size are chosen before the eventual angle translation function or its derivatives.

    theorem compact_collar_positive_small_shift {K C Ω : Set E} {J : Set A}
    (hK : IsCompact K) (hC : IsClosed C) (hΩ : IsOpen Ω) (hKΩ : K ⊆ Ω)
    (hJ : IsCompact J) {F : E × (A × ℝ) → ℝ}
    (hF : ContinuousOn F (Ω ×ˢ univ))
    (hpos : ∀ x ∈ K ∩ C, ∀ t ∈ J, 0 < F (x, (t, 0))) :
    ∃ W : Set E, IsOpen W ∧ C ⊆ W ∧ ∃ ε : ℝ, 0 < ε ∧
      ∀ x ∈ K ∩ W, ∀ t ∈ J, ∀ h : ℝ, |h| < ε → 0 < F (x, (t, h)) := by
…