Adapting Families of Maps to Open Covers

2. Reduction to a Reparametrization🔗

Every homotopy F we construct has the special form F(t,p,x) = f(u(t,p,x), x) for a continuous reparametrization u : [0,1]\times P \times X \to P of the parameter polyhedron. This chapter performs the clean structural reduction: all four conclusions of Theorem A follow formally from three properties of u, and likewise all seven conclusions of Theorem B. The existence of such a u is the geometric core, stated here and proved in Part II and Part III.

open Set unitInterval Geometry open scoped Topology open _root_.FamiliesOfMapsB01 namespace Submission namespace FamiliesOfMapsB01 variable {k : ℕ} {ι X T : Type*} [TopologicalSpace X] [TopologicalSpace T]

The geometric core of the continuous case — everything that Part II provides — is the following existence statement. (Its two inputs, handle_family_exists and reparam_of_handles, are Theorem 3.4 and Proposition 3.2 in the handle families chapter.)

/-- **Geometric core of the continuous case (the one remaining hard input).** There is a continuous reparametrisation `u : I × P × X → P` of the parameter polytope which starts at the identity, makes `f` adapted to `U` on each cell of some polyhedral subdivision of `P`, and maps every boundary subpolyhedron of `P` into itself. This is the Morrison–Walker general-position handle construction (formula (B.1)). -/ theorem reparam_exists {P : Set (Fin k → ℝ)} (hP : IsPolyhedron P) [CompactSpace X] (U : ι → Set X) (hUopen : ∀ α, IsOpen (U α)) (ρ : PartitionOfUnity ι X univ) (hρ : ρ.IsSubordinate U) (f : C(P × X, T)) : ∃ u : C(I × P × X, P), (∀ p : P, ∀ x : X, u (0, p, x) = p) ∧ (∃ K : Subdivision P, ∀ D ∈ K.complex.facets, AdaptedTo U k (fun q : closedCell P D × X => f (u (1, q.1.1, q.2), q.2))) ∧ (∀ Q : Set P, IsBoundarySubpolyhedron Q → ∀ t : I, ∀ p : P, ∀ x : X, p ∈ Q → u (t, p, x) ∈ Q) := k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)hP:IsPolyhedron Pinst✝:CompactSpace XU:ι → Set XhUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)⊢ ∃ u, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q have hPc : Convex ℝ P := k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)hP:IsPolyhedron Pinst✝:CompactSpace XU:ι → Set XhUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)⊢ ∃ u, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Tinst✝:CompactSpace XU:ι → Set XhUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate US:Finset (Fin k → ℝ)f:C(↑((convexHull ℝ) ↑S) × X, T)⊢ Convex ℝ ((convexHull ℝ) ↑S); All goals completed! 🐙 k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)hP:IsPolyhedron Pinst✝:CompactSpace XU:ι → Set XhUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)hPc:Convex ℝ PK:Subdivision Pg:ι → C(↑P, ↑P)hface:∀ (α : ι), ρ α = 0 ∨ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ p ∈ Q, (g α) p ∈ Qhk:∀ D ∈ K.complex.facets, ∃ A, A.card ≤ k ∧ ∀ α ∉ A, ∀ (p p' : ↑P), ↑p ∈ (convexHull ℝ) ↑D → ↑p' ∈ (convexHull ℝ) ↑D → (g α) p = (g α) p'⊢ ∃ u, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q All goals completed! 🐙

Proposition 2.1🔗

Proposition 2.1. Suppose u : [0,1]\times P \times X \to P is continuous and:

(i) u(0,p,x) = p for all p, x;

(ii) there is a subdivision K of P such that for every facet D of K, the family (p,x) \mapsto f(u(1,p,x),x), restricted to \operatorname{conv}(D) \times X, is adapted to \mathcal U with constant k;

(iii) (u is face-preserving) for every boundary subpolyhedron Q of P: if p \in Q then u(t,p,x) \in Q for all t, x.

Then F(t,p,x) := f(u(t,p,x),x) satisfies conclusions (1)–(4) of Theorem A.

Proof. F is continuous as a composition of continuous maps. (1) is immediate from (i). (2) is exactly (ii). For (3), suppose f is supported on S and x \notin S; then f(q,x) = f(q',x) for all q, q' \in P, in particular for q = u(t,p,x) and q' = u(t',p',x); so F is supported on S — note this uses nothing about u beyond its taking values in P. For (4), suppose f|_{Q \times X} is supported on S' and x \notin S'; given (t,p) and (t',p') with p, p' \in Q, property (iii) puts u(t,p,x) and u(t',p',x) in Q, where the support hypothesis applies and gives f(u(t,p,x),x) = f(u(t',p',x),x). \blacksquare

/-- **Structural reduction, continuous case.** Given the geometric core `reparam_exists`, the four conjuncts of the continuous benchmark conclusion follow. -/ theorem continuous_of_reparam {P : Set (Fin k → ℝ)} [CompactSpace X] (U : ι → Set X) (f : C(P × X, T)) (u : C(I × P × X, P)) (hu0 : ∀ p : P, ∀ x : X, u (0, p, x) = p) (hadapt : ∃ K : Subdivision P, ∀ D ∈ K.complex.facets, AdaptedTo U k (fun q : closedCell P D × X => f (u (1, q.1.1, q.2), q.2))) (huface : ∀ Q : Set P, IsBoundarySubpolyhedron Q → ∀ t : I, ∀ p : P, ∀ x : X, p ∈ Q → u (t, p, x) ∈ Q) : ∃ F : C(I × P × X, T), (∀ p : P, ∀ x : X, F (0, p, x) = f (p, x)) ∧ (∃ K : Subdivision P, ∀ D ∈ K.complex.facets, AdaptedTo U k (fun q : closedCell P D × X => F (1, q.1.1, q.2))) ∧ (∀ S : Set X, Supported (f := f.toFun) S → Supported (fun q : (I × P) × X => F (q.1.1, q.1.2, q.2)) S) ∧ (∀ Q : Set P, IsBoundarySubpolyhedron Q → ∀ S' : Set X, Supported (fun q : Q × X => f (q.1.1, q.2)) S' → Supported (fun q : (I × Q) × X => F (q.1.1, q.1.2.1, q.2)) S') := k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∃ F, (∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧ (∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S' k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun z => f (u z, z.2.2)k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∀ (p : ↑P) (x : X), { toFun := fun z => f (u z, z.2.2), continuous_toFun := ?refine_1 } (0, p, x) = f (p, x)k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ?refine_1 } (1, ↑q.1, q.2)k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∀ (S : Set X), Supported f.toFun S → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ?refine_1 } (q.1.1, q.1.2, q.2)) Sk:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ?refine_1 } (q.1.1, ↑q.1.2, q.2)) S' k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun z => f (u z, z.2.2) All goals completed! 🐙 k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∀ (p : ↑P) (x : X), { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (0, p, x) = f (p, x) intro p k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Qp:↑Px:X⊢ { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (0, p, x) = f (p, x); All goals completed! 🐙 k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (1, ↑q.1, q.2) All goals completed! 🐙 k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∀ (S : Set X), Supported f.toFun S → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) S intro S k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QS:Set XhS:Supported f.toFun S⊢ Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) S k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QS:Set XhS:Supported f.toFun Sp:↑I × ↑P⊢ ∀ (p' : ↑I × ↑P), ∀ x ∉ S, (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑P⊢ ∀ x ∉ S, (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑Px:X⊢ x ∉ S → (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑Px:Xhx:x ∉ S⊢ (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑Px:Xhx:x ∉ S⊢ f (u (p.1, p.2, x), x) = f (u (p'.1, p'.2, x), x) All goals completed! 🐙 k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q⊢ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' intro Q k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron Q⊢ ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set X⊢ Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'⊢ Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Q⊢ ∀ (p' : ↑I × ↑Q), ∀ x ∉ S', (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Q⊢ ∀ x ∉ S', (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:X⊢ x ∉ S' → (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:Xhx:x ∉ S'⊢ (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:Xhx:x ∉ S'⊢ f (u (p.1, ↑p.2, x), x) = f (u (p'.1, ↑p'.2, x), x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:Xhx:x ∉ S'h1:u (p.1, ↑p.2, x) ∈ Q⊢ f (u (p.1, ↑p.2, x), x) = f (u (p'.1, ↑p'.2, x), x) k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)inst✝:CompactSpace XU:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)hu0:∀ (p : ↑P) (x : X), u (0, p, x) = phadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:Xhx:x ∉ S'h1:u (p.1, ↑p.2, x) ∈ Qh2:u (p'.1, ↑p'.2, x) ∈ Q⊢ f (u (p.1, ↑p.2, x), x) = f (u (p'.1, ↑p'.2, x), x) All goals completed! 🐙

So it remains to construct u satisfying (i)–(iii). Note that (iii) is the only place the extremality condition on boundary subpolyhedra is used, and it is used through convexity: we will keep u(t,p,x) a convex combination of points of Q.

9.1 Reduction, again🔗

As in Step 2, we seek a continuous reparametrization u with properties (i)–(iii) of Proposition 2.1, now together with homeomorphisms \mathrm{Slice}(t,p) : X \to T satisfying f(u(t,p,x),x) = \mathrm{Slice}(t,p)(x), all of them and all their inverses L'-Lipschitz for a single L'. Setting F(t,p,x) := f(u(t,p,x),x) then yields conclusions (1)–(7) of Theorem B: (1), (3), (4), (5) exactly as in Proposition 2.1, and (2), (6), (7) verbatim from the properties of \mathrm{Slice}.

Again split on N, the number of active indices.

Easy regime (N \le k). Take u(t,p,x) := p, the identity reparametrization, and \mathrm{Slice}(t,p) := \mathrm{slice}(p). Properties (i), (iii) and the slice identity are trivial; the slices are L-bi-Lipschitz homeomorphisms by hypothesis. For adaptation, take any subdivision (Theorem 7.1) and, on every facet, the exceptional set A := the active indices, |A| = N \le k; the sets \{U_\alpha\}_{\alpha \in A} cover X: at every x, \sum_\alpha r_\alpha(x) = 1 forces some active \alpha with r_\alpha(x) \ne 0, and then x \in \operatorname{supp}(r_\alpha) \subseteq U_\alpha. So there are no points x \notin \bigcup_{\alpha \in A} U_\alpha at all, and the support condition holds vacuously.

Formally, the easy regime is dispatched inside the existence theorem itself, whose main regime (more than k active indices) is reparam_biLip_exists_gt, proved in the bi-Lipschitz reparametrization chapter:

/-- **Geometric core of the bi-Lipschitz case (the one remaining hard input).** The same reparametrisation as in `reparam_exists`, but now additionally bundling each time slice `x ↦ f (u (t,p,x), x)` as a homeomorphism `Slice (t,p) : X ≃ₜ T` that is bi-Lipschitz with a uniform constant `L'`. This is the bi-Lipschitz variant of the Morrison–Walker construction: the slices stay homeomorphisms because the normal derivative `∂u/∂x` is kept small (the cell decompositions are taken fine enough), so the chain rule keeps each `F (t,p,·)` a bi-Lipschitz homeomorphism. -/ theorem reparam_biLip_exists {X T : Type*} [MetricSpace X] [MetricSpace T] [CompactSpace X] {P : Set (Fin k → ℝ)} (hP : IsPolyhedron P) {ι : Type*} (U : ι → Set X) (hUopen : ∀ α, IsOpen (U α)) (ρ : PartitionOfUnity ι X univ) (hρ : ρ.IsSubordinate U) (f : C(P × X, T)) (slice : P → (X ≃ₜ T)) (h_slice_eq : ∀ p : P, ∀ x : X, f (p, x) = slice p x) (L : NNReal) (hf_joint : LipschitzWith L f.toFun) (hf_slice_inv : ∀ p : P, LipschitzWith L (slice p).symm) : ∃ u : C(I × P × X, P), ∃ L' : NNReal, ∃ Slice : I × P → (X ≃ₜ T), (∀ p : P, ∀ x : X, u (0, p, x) = p) ∧ (∀ t : I, ∀ p : P, ∀ x : X, f (u (t, p, x), x) = Slice (t, p) x) ∧ (∃ K : Subdivision P, ∀ D ∈ K.complex.facets, AdaptedTo U k (fun q : closedCell P D × X => f (u (1, q.1.1, q.2), q.2))) ∧ (∀ Q : Set P, IsBoundarySubpolyhedron Q → ∀ t : I, ∀ p : P, ∀ x : X, p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ tp : I × P, LipschitzWith L' (Slice tp)) ∧ (∀ tp : I × P, LipschitzWith L' (Slice tp).symm) := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm classical k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ k⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmk:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:¬⋯.toFinset.card ≤ k⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ k⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm -- Easy regime: at most `k` active cover indices. The identity reparametrisation -- already works: adaptation is vacuous because the active sets cover `X`, and each -- slice is exactly `slice p`, which is uniformly bi-Lipschitz with constant `L`. have hcover : ∀ x : X, ∃ α ∈ (activeIndices_finite ρ).toFinset, x ∈ U α := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:X⊢ ∃ α ∈ ⋯.toFinset, x ∈ U α k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1⊢ ∃ α ∈ ⋯.toFinset, x ∈ U α have hne : ∃ α, ρ α x ≠ 0 := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1hcon:¬∃ α, (ρ α) x ≠ 0⊢ False `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ``` k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1hcon:∀ (α : ι), (ρ α) x = 0⊢ False have hz : ∑ᶠ α, ρ α x = 0 := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1hcon:∀ (α : ι), (ρ α) x = 0hz:1 = 0⊢ False All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1α:ιhα:(ρ α) x ≠ 0⊢ ∃ α ∈ ⋯.toFinset, x ∈ U α have hαf : ρ α ≠ 0 := fun h => hα (k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1α:ιhα:(ρ α) x ≠ 0h:ρ α = 0⊢ (ρ α) x = 0 All goals completed! 🐙) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ kx:Xhsum:∑ᶠ (α : ι), (ρ α) x = 1α:ιhα:(ρ α) x ≠ 0hαf:ρ α ≠ 0⊢ x ∈ U α All goals completed! 🐙 refine ⟨⟨fun z => z.2.1, k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ Continuous[instTopologicalSpaceProd, _] fun z => z.2.1 All goals completed! 🐙⟩, L, fun tp => slice tp.2, ?_, ?_, ?_, ?_, ?_, ?_⟩ k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∀ (p : ↑P) (x : X), { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (0, p, x) = p intro p k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αp:↑Px:X⊢ { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (0, p, x) = p; All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∀ (t : ↑I) (p : ↑P) (x : X), f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x), x) = ((fun tp => slice tp.2) (t, p)) x intro t k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αt:↑Ip:↑P⊢ ∀ (x : X), f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x), x) = ((fun tp => slice tp.2) (t, p)) x k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αt:↑Ip:↑Px:X⊢ f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x), x) = ((fun tp => slice tp.2) (t, p)) x; All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∀ D ∈ ⋯.some.complex.facets, AdaptedTo U k fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2) intro D k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facets⊢ AdaptedTo U k fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facets⊢ Supported (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (⋃ α ∈ ⋯.toFinset, U α) intro q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facetsq:↑(closedCell P D)q':↑(closedCell P D)⊢ ∀ x ∉ ⋃ α ∈ ⋯.toFinset, U α, (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (q, x) = (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (q', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facetsq:↑(closedCell P D)q':↑(closedCell P D)x:X⊢ x ∉ ⋃ α ∈ ⋯.toFinset, U α → (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (q, x) = (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (q', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facetsq:↑(closedCell P D)q':↑(closedCell P D)x:Xhx:x ∉ ⋃ α ∈ ⋯.toFinset, U α⊢ (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (q, x) = (fun q => f ({ toFun := fun z => z.2.1, continuous_toFun := ⋯ } (1, ↑q.1, q.2), q.2)) (q', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facetsq:↑(closedCell P D)q':↑(closedCell P D)x:Xhx:x ∉ ⋃ α ∈ ⋯.toFinset, U α⊢ False k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αD:Finset (Fin k → ℝ)hD:D ∈ ⋯.some.complex.facetsq:↑(closedCell P D)q':↑(closedCell P D)x:Xhx:x ∉ ⋃ α ∈ ⋯.toFinset, U αα:ιhαA:α ∈ ⋯.toFinsethxα:x ∈ U α⊢ False All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x) ∈ Q intro Q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αQ:Set ↑PhQ:IsBoundarySubpolyhedron Q⊢ ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x) ∈ Q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αQ:Set ↑PhQ:IsBoundarySubpolyhedron Qt:↑I⊢ ∀ (p : ↑P) (x : X), p ∈ Q → { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x) ∈ Q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αQ:Set ↑PhQ:IsBoundarySubpolyhedron Qt:↑Ip:↑P⊢ ∀ (x : X), p ∈ Q → { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x) ∈ Q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αQ:Set ↑PhQ:IsBoundarySubpolyhedron Qt:↑Ip:↑Px:X⊢ p ∈ Q → { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x) ∈ Q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αQ:Set ↑PhQ:IsBoundarySubpolyhedron Qt:↑Ip:↑Px:Xhp:p ∈ Q⊢ { toFun := fun z => z.2.1, continuous_toFun := ⋯ } (t, p, x) ∈ Q; All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∀ (tp : ↑I × ↑P), LipschitzWith L ⇑((fun tp => slice tp.2) tp) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αtp:↑I × ↑P⊢ LipschitzWith L ⇑((fun tp => slice tp.2) tp) have hp : LipschitzWith L (fun x => f.toFun (tp.2, x)) := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm All goals completed! 🐙 have hfun : (fun x => f.toFun (tp.2, x)) = (slice tp.2 : X → T) := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αtp:↑I × ↑Php:LipschitzWith L fun x => f.toFun (tp.2, x)x:X⊢ f.toFun (tp.2, x) = (slice tp.2) x; All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αtp:↑I × ↑Php:LipschitzWith L ⇑(slice tp.2)hfun:(fun x => f.toFun (tp.2, x)) = ⇑(slice tp.2)⊢ LipschitzWith L ⇑((fun tp => slice tp.2) tp) All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U α⊢ ∀ (tp : ↑I × ↑P), LipschitzWith L ⇑((fun tp => slice tp.2) tp).symm k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:⋯.toFinset.card ≤ khcover:∀ (x : X), ∃ α ∈ ⋯.toFinset, x ∈ U αtp:↑I × ↑P⊢ LipschitzWith L ⇑((fun tp => slice tp.2) tp).symm; All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)hP:IsPolyhedron Pι:Type u_6U:ι → Set XhUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι Xhρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ Th_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNRealhf_joint:LipschitzWith L f.toFunhf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symmhcard:¬⋯.toFinset.card ≤ k⊢ ∃ u L' Slice, (∀ (p : ↑P) (x : X), u (0, p, x) = p) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ Q) ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm All goals completed! 🐙

The structural reduction for the seven conclusions of Theorem B is exactly as in Proposition 2.1, with the two slice conclusions carried over verbatim:

/-- **Structural reduction, bi-Lipschitz case.** Given the geometric core `reparam_biLip_exists`, the seven conjuncts of the bi-Lipschitz benchmark conclusion follow. -/ theorem biLipschitz_of_reparam {X T : Type*} [MetricSpace X] [MetricSpace T] [CompactSpace X] {P : Set (Fin k → ℝ)} {ι : Type*} (U : ι → Set X) (f : C(P × X, T)) (u : C(I × P × X, P)) (L' : NNReal) (Slice : I × P → (X ≃ₜ T)) (hu0 : ∀ p : P, ∀ x : X, u (0, p, x) = p) (hsliceEq : ∀ t : I, ∀ p : P, ∀ x : X, f (u (t, p, x), x) = Slice (t, p) x) (hadapt : ∃ K : Subdivision P, ∀ D ∈ K.complex.facets, AdaptedTo U k (fun q : closedCell P D × X => f (u (1, q.1.1, q.2), q.2))) (huface : ∀ Q : Set P, IsBoundarySubpolyhedron Q → ∀ t : I, ∀ p : P, ∀ x : X, p ∈ Q → u (t, p, x) ∈ Q) (hLip : ∀ tp : I × P, LipschitzWith L' (Slice tp)) (hLipinv : ∀ tp : I × P, LipschitzWith L' (Slice tp).symm) : ∃ F : C(I × P × X, T), ∃ L'' : NNReal, ∃ Slice' : I × P → (X ≃ₜ T), (∀ p : P, ∀ x : X, F (0, p, x) = f (p, x)) ∧ (∀ t : I, ∀ p : P, ∀ x : X, F (t, p, x) = Slice' (t, p) x) ∧ (∃ K : Subdivision P, ∀ D ∈ K.complex.facets, AdaptedTo U k (fun q : closedCell P D × X => F (1, q.1.1, q.2))) ∧ (∀ S : Set X, Supported (f := f.toFun) S → Supported (fun q : (I × P) × X => F (q.1.1, q.1.2, q.2)) S) ∧ (∀ Q : Set P, IsBoundarySubpolyhedron Q → ∀ S' : Set X, Supported (fun q : Q × X => f (q.1.1, q.2)) S' → Supported (fun q : (I × Q) × X => F (q.1.1, q.1.2.1, q.2)) S') ∧ (∀ tp : I × P, LipschitzWith L'' (Slice' tp)) ∧ (∀ tp : I × P, LipschitzWith L'' (Slice' tp).symm) := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ ∃ F L'' Slice', (∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧ (∀ (t : ↑I) (p : ↑P) (x : X), F (t, p, x) = (Slice' (t, p)) x) ∧ (∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧ (∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧ (∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S') ∧ (∀ (tp : ↑I × ↑P), LipschitzWith L'' ⇑(Slice' tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L'' ⇑(Slice' tp).symm refine ⟨⟨fun z => f (u z, z.2.2), k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun z => f (u z, z.2.2) All goals completed! 🐙⟩, L', Slice, ?_, ?_, hadapt, ?_, ?_, hLip, hLipinv⟩ k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ ∀ (p : ↑P) (x : X), { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (0, p, x) = f (p, x) intro p k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmp:↑Px:X⊢ { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (0, p, x) = f (p, x); All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ ∀ (t : ↑I) (p : ↑P) (x : X), { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (t, p, x) = (Slice (t, p)) x intro t k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmt:↑Ip:↑P⊢ ∀ (x : X), { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (t, p, x) = (Slice (t, p)) x k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmt:↑Ip:↑Px:X⊢ { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (t, p, x) = (Slice (t, p)) x; k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmt:↑Ip:↑Px:X⊢ f (u (t, p, x), x) = (Slice (t, p)) x; All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ ∀ (S : Set X), Supported f.toFun S → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) S intro S k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmS:Set XhS:Supported f.toFun S⊢ Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) S k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmS:Set XhS:Supported f.toFun Sp:↑I × ↑P⊢ ∀ (p' : ↑I × ↑P), ∀ x ∉ S, (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑P⊢ ∀ x ∉ S, (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑Px:X⊢ x ∉ S → (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑Px:Xhx:x ∉ S⊢ (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, q.1.2, q.2)) (p', x); k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmS:Set XhS:Supported f.toFun Sp:↑I × ↑Pp':↑I × ↑Px:Xhx:x ∉ S⊢ f (u (p.1, p.2, x), x) = f (u (p'.1, p'.2, x), x); All goals completed! 🐙 k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm⊢ ∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' intro Q k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron Q⊢ ∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set X⊢ Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'⊢ Supported (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) S' k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Q⊢ ∀ (p' : ↑I × ↑Q), ∀ x ∉ S', (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Q⊢ ∀ x ∉ S', (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:X⊢ x ∉ S' → (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:Xhx:x ∉ S'⊢ (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p, x) = (fun q => { toFun := fun z => f (u z, z.2.2), continuous_toFun := ⋯ } (q.1.1, ↑q.1.2, q.2)) (p', x) k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)ι:Type u_6U:ι → Set Xf:C(↑P × X, T)u:C(↑I × ↑P × X, ↑P)L':NNRealSlice:↑I × ↑P → X ≃ₜ Thu0:∀ (p : ↑P) (x : X), u (0, p, x) = phsliceEq:∀ (t : ↑I) (p : ↑P) (x : X), f (u (t, p, x), x) = (Slice (t, p)) xhadapt:∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => f (u (1, ↑q.1, q.2), q.2)huface:∀ (Q : Set ↑P), IsBoundarySubpolyhedron Q → ∀ (t : ↑I) (p : ↑P) (x : X), p ∈ Q → u (t, p, x) ∈ QhLip:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)hLipinv:∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symmQ:Set ↑PhQ:IsBoundarySubpolyhedron QS':Set XhS':Supported (fun q => f (↑q.1, q.2)) S'p:↑I × ↑Qp':↑I × ↑Qx:Xhx:x ∉ S'⊢ f (u (p.1, ↑p.2, x), x) = f (u (p'.1, ↑p'.2, x), x) All goals completed! 🐙 end FamiliesOfMapsB01 end Submission