Theorems · Theorem · real analysis

BoxIntegral.Box.continuousOn_face_Icc

∀ {X : Type u_2} [inst : TopologicalSpace X] {n : ℕ} {f : (Fin (n + 1) → ℝ) → X} {I : BoxIntegral.Box (Fin (n + 1))},
  ContinuousOn f (BoxIntegral.Box.Icc I) →
    ∀ {i : Fin (n + 1)} {x : ℝ},
      x ∈ Set.Icc (I.lower i) (I.upper i) → ContinuousOn (f ∘ i.insertNth x) (BoxIntegral.Box.Icc (I.face i))

Defined in

Mathlib.Analysis.BoxIntegral.Box.Basic

Cited by

2 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace