The boundary of a cube is a closed cofibration

For a finite index type N, the boundary Cube.boundary N of the cube I^N has the homotopy extension property in the cube. The affine homeomorphism TauCeti.cubeHomeomorphClosedBall of the cube onto the closed unit ball of the sup norm on N → ℝ carries the boundary onto the unit sphere (TauCeti.norm_cubeHomeomorphClosedBall_eq_one_iff), and the unit sphere has the homotopy extension property in the closed unit ball (TauCeti.hasHomotopyExtensionProperty_sphere_closedBall).

The same holds for the boundary TauCeti.Cube.prodBoundary N of the cube I × I^N with a distinguished first direction, on which relative cubes are defined: it corresponds to the boundary of I^(Option N) under TauCeti.piOptionEquivProdHomeomorph, and likewise for the boundary of the cube I × (I × I^N), which homotopies of relative cubes are defined on.

Main declarations

• TauCeti.hasHomotopyExtensionProperty_cubeBoundary: the boundary of I^N has the homotopy extension property.
• TauCeti.hasHomotopyExtensionProperty_prodBoundary: the boundary of I × I^N has the homotopy extension property.
• TauCeti.hasHomotopyExtensionProperty_boundary_prod: the boundary of I × (I × I^N) has the homotopy extension property.
• TauCeti.hasHomotopyExtensionProperty_zero_one: the end points {0, 1} of the unit interval, the boundary of the one-dimensional cube, have the homotopy extension property.

theorem TauCeti.hasHomotopyExtensionProperty_cubeBoundary {N : Type u_1} [Finite N] : HasHomotopyExtensionProperty (Cube.boundary N)

The boundary of the cube I^N has the homotopy extension property in the cube.

theorem TauCeti.hasHomotopyExtensionProperty_prodBoundary {N : Type u_1} [Finite N] : HasHomotopyExtensionProperty (Cube.prodBoundary N)

The boundary of the cube I × I^N has the homotopy extension property in the cube.

theorem TauCeti.hasHomotopyExtensionProperty_boundary_prod {N : Type u_1} [Finite N] : HasHomotopyExtensionProperty {x : ↑unitInterval × ↑unitInterval × (N → ↑unitInterval) | (x.1 = 0 ∨ x.1 = 1) ∨ x.2 ∈ Cube.prodBoundary N}

The boundary of the cube I × (I × I^N) has the homotopy extension property in the cube.

theorem TauCeti.hasHomotopyExtensionProperty_zero_one : HasHomotopyExtensionProperty {0, 1}

The end points {0, 1} of the unit interval have the homotopy extension property in I: they form the boundary of the one-dimensional cube I^Unit.