English
If f is continuous on Box.Icc I, then f ∘ i.insertNth x is continuous on Box.Icc(I.face i).
Русский
Если f непрерывна на Box.Icc I, то композиция f ∘ i.insertNth x непрерывна на Box.Icc(I.face i).
LaTeX
$$$\forall X \; [TopologicalSpace X] \; {n} \; {f : (Fin (n + 1) \to \mathbb{R}) \to X},\; f \text{ continuousOn } (Box.Icc I) \Rightarrow \ \forall i, x \in \mathbb{R}, \text{ContinuousOn}(f \circ i.insertNth x) (Box.Icc (I.face i))$$$
Lean4
theorem continuousOn_face_Icc {X} [TopologicalSpace X] {n} {f : (Fin (n + 1) → ℝ) → X} {I : Box (Fin (n + 1))}
(h : ContinuousOn f (Box.Icc I)) {i : Fin (n + 1)} {x : ℝ} (hx : x ∈ Icc (I.lower i) (I.upper i)) :
ContinuousOn (f ∘ i.insertNth x) (Box.Icc (I.face i)) :=
h.comp (continuousOn_const.finInsertNth i continuousOn_id) (I.mapsTo_insertNth_face_Icc hx)
