Theorems · Theorem · real analysis

BoxIntegral.Box.mapsTo_insertNth_face_Icc

∀ {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ},
  x ∈ Set.Icc (I.lower i) (I.upper i) →
    Set.MapsTo (i.insertNth x) (BoxIntegral.Box.Icc (I.face i)) (BoxIntegral.Box.Icc I)

Defined in: Mathlib.Analysis.BoxIntegral.Box.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
Set.Iccstatement and proof · cited by 1,702
Set.MapsTostatement · cited by 732
OrderEmbeddingstatement · cited by 619
BoxIntegral.Boxstatement and proof · cited by 464
Fin.insertNthstatement · cited by 95
BoxIntegral.Box.Iccstatement and proof · cited by 76
BoxIntegral.Box.upperstatement and proof · cited by 70
BoxIntegral.Box.lowerstatement and proof · cited by 65
BoxIntegral.Box.facestatement and proof · cited by 13

Cited by3

Results whose statement or proof uses this declaration.

BoxIntegral.Box.continuousOn_face_Iccproof · cited by 2
BoxIntegral.hasIntegral_GP_pderivproof · cited by 1
BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_leproof · cited by 1