CompactSubmersionFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A finite collection of uniform local charts

Compactness reduces a family with pointwise nondegenerate endpoint schemes to finitely many schemes covering one common target neighborhood.

theorem OAI.PolycyclicRecognition.finite_positive_lower_bound line 17

theorem OAI.PolycyclicRecognition.exists_finite_uniform_submersion_family line 38

Source documentation

Pointwise submersive schemes on a compact parameter set have a common image ball, using only finitely many of the actual schemes.

theorem exists_finite_uniform_submersion_family
    (f : J → P × E → F) {K : Set P} (hK : IsCompact K)
    (h : ∀ p ∈ K, ∃ j, ContDiffAt ℝ 1 (f j) (p, 0) ∧ f j (p, 0) = 0 ∧
      Function.Surjective (fun v : E => fderiv ℝ (f j) (p, 0) (0, v)))
    {R : ℝ} (hR : 0 < R) :
    ∃ (s : Finset J) (ε : ℝ), 0 < ε ∧ ∀ p ∈ K, ∃ j ∈ s,
      ball (0 : F) ε ⊆ (fun x : E => f j (p, x)) '' ball 0 R := by
…