A Lebesgue number for a singular simplex against an open cover

Let σ : Δⁿ → X be a singular simplex (with X an arbitrary topological space) and let 𝒰 be an open cover of X. Pulling 𝒰 back along σ gives an open cover of the compact metric space Δⁿ, so the Lebesgue-number lemma yields a uniform ε > 0 such that every subset of the domain Δⁿ with diameter < ε is mapped by σ into a single member of 𝒰.

Only the domain Δⁿ needs to be metric and compact; X stays arbitrary.

Main results

• SphereOddDegree.ExistsCoverMemberContainingImage — the predicate that the image σ '' A of a subset A ⊆ Δⁿ lies in one member of the cover.
• SphereOddDegree.singularSimplex_hasLebesgueNumber_for_openCover — the Lebesgue-number theorem: there is ε > 0 such that Metric.diam A < ε implies σ '' A is contained in a cover member.

This is the compactness input that the project combines with the diameter-shrinking theorem of the project: once a refined affine simplex has domain diameter < ε, its image under σ lies in some U ∈ 𝒰.

def SphereOddDegree.ExistsCoverMemberContainingImage {X : TopCat} (𝒰 : OpenCoverData X) {n : ℕ} (σ : singularSimplices X n) (A : Set ↑(AffineBarycentricSubdivision.Delta n)) : Prop

A subset A ⊆ Δⁿ has its σ-image contained in a single member of the open cover 𝒰.

Equations

• SphereOddDegree.ExistsCoverMemberContainingImage 𝒰 σ A = ∃ U ∈ 𝒰.sets, ⇑(SphereOddDegree.mvSimplexMap σ) '' A ⊆ U

theorem SphereOddDegree.singularSimplex_hasLebesgueNumber_for_openCover {X : TopCat} (𝒰 : OpenCoverData X) {n : ℕ} (σ : singularSimplices X n) : ∃ (eps : ℝ), 0 < eps ∧ ∀ (A : Set ↑(AffineBarycentricSubdivision.Delta n)), Metric.diam A < eps → ∃ U ∈ 𝒰.sets, ⇑(mvSimplexMap σ) '' A ⊆ U

theorem SphereOddDegree.singularSimplex_hasLebesgueNumber_for_openCover' {X : TopCat} (𝒰 : OpenCoverData X) {n : ℕ} (σ : singularSimplices X n) : ∃ (eps : ℝ), 0 < eps ∧ ∀ (A : Set ↑(AffineBarycentricSubdivision.Delta n)), Metric.diam A < eps → ExistsCoverMemberContainingImage 𝒰 σ A

Restatement of the Lebesgue-number theorem in terms of ExistsCoverMemberContainingImage.