The unit cylinder is open

theorem CIV.contDiffOn_spatialPartial_of_contDiffOn {n : ℕ} {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑n + 1) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (i : Fin 3) : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial g i z) unitCylinder

A C^{n+1} scalar has C^n spatial partial derivatives on the unit cylinder.

theorem CIV.contDiffOn_spatialPartial_of_smooth {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial g i z) unitCylinder

A smooth scalar has smooth spatial partial derivatives on the unit cylinder.

Smoothness of the time partial derivative

theorem CIV.contDiffOn_timePartial_of_contDiffOn {n : ℕ} {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑n + 1) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial g z) unitCylinder

A C^{n+1} scalar has C^n time partial derivative on the unit cylinder.

Smoothness of components of a vector field

theorem CIV.contDiffOn_componentFun {n : ℕ∞} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i : Fin 3) : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) unitCylinder

A C^n vector field has C^n component functions on the unit cylinder.