Theorems · Definition · measure theory
BoxIntegral.BoxAdditiveMap.volume
{ι : Type u_1} →
[Fintype ι] →
{E : Type u_2} →
[inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] E) ⊤Box-additive map sending each box I to the continuous linear endomorphism
x ↦ (volume I).toReal • x.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 248 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Realstatement and proof · cited by 25,697
- RingHom.idstatement · cited by 18,349
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Top.topstatement · cited by 9,680
- Fintypestatement and proof · cited by 7,736
- ContinuousLinearMapstatement · cited by 5,352
- WithTopstatement · cited by 3,754
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- BoxIntegral.Boxstatement · cited by 464
- BoxIntegral.BoxAdditiveMapstatement · cited by 92
- MeasureTheory.Measure.toBoxAdditiveproof · cited by 22
Cited by4
Results whose statement or proof uses this declaration.
- BoxIntegral.hasIntegral_GP_pderivstatement and proof · cited by 1
- BoxIntegral.BoxAdditiveMap.volume_applystatement · cited by 1
- BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_lestatement and proof · cited by 1
- BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAtstatement · cited by 0