Smooth parametrization of coordinate faces of a cube

theorem NairTenenbaum.card_coordinateFaceParameter {ι : Type u_1} [Fintype ι] (i : ι) : Fintype.card { j : ι // j ≠ i } = Fintype.card ι - 1

noncomputable def NairTenenbaum.coordinateFaceParameterEquiv {ι : Type u_1} [Fintype ι] (i : ι) : { j : ι // j ≠ i } ≃ Fin (Fintype.card ι - 1)

The equivalence identifying the free coordinates of a cube face.

Equations

• NairTenenbaum.coordinateFaceParameterEquiv i = Fintype.equivFinOfCardEq ⋯

noncomputable def NairTenenbaum.cubeFaceMap {ι : Type u_1} [Fintype ι] (i : ι) (b : ℝ) (v : Fin (Fintype.card ι - 1) → ℝ) : ι → ℝ

The embedding of the free coordinates into a specified cube face.

Equations

• NairTenenbaum.cubeFaceMap i b v j = if h : j = i then b else v ((NairTenenbaum.coordinateFaceParameterEquiv i) ⟨j, h⟩)

theorem NairTenenbaum.contDiff_cubeFaceMap {ι : Type u_1} [Fintype ι] (i : ι) (b : ℝ) : ContDiff ℝ ⊤ (cubeFaceMap i b)

theorem NairTenenbaum.exists_cubeFaceMap_of_coordinate_eq {ι : Type u_1} [Fintype ι] {i : ι} {b : ℝ} {v : ι → ℝ} (hv : v ∈ Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1) (hi : v i = b) : ∃ u ∈ Set.Icc (fun (x : Fin (Fintype.card ι - 1)) => 0) fun (x : Fin (Fintype.card ι - 1)) => 1, cubeFaceMap i b u = v