Theorems · Definition · real analysis
BoxIntegral.Box.splitCenterBox
{ι : Type u_1} → BoxIntegral.Box ι → Set ι → BoxIntegral.Box ιFor a box I, the hyperplanes passing through its center split I into 2 ^ card ι boxes.
BoxIntegral.Box.splitCenterBox I s is one of these boxes. See also
BoxIntegral.Partition.splitCenter for the corresponding BoxIntegral.Partition.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- BoxIntegral.Boxstatement and proof · cited by 464
- Set.piecewiseproof · cited by 136
- BoxIntegral.Box.upperproof · cited by 70
- BoxIntegral.Box.lowerproof · cited by 65
Cited by13
Results whose statement or proof uses this declaration.
- BoxIntegral.Box.mem_splitCenterBoxstatement · cited by 3
- BoxIntegral.Box.splitCenterBox_lestatement and proof · cited by 2
- BoxIntegral.Box.upper_sub_lower_splitCenterBoxstatement · cited by 2
- BoxIntegral.Prepartition.mem_splitCenterstatement and proof · cited by 2
- BoxIntegral.Box.disjoint_splitCenterBoxstatement and proof · cited by 1
- BoxIntegral.Box.splitCenterBoxEmbproof · cited by 1
- BoxIntegral.Box.splitCenterBoxEmb_applystatement · cited by 1
- BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenterproof · cited by 1
- BoxIntegral.Box.subbox_induction_on'statement and proof · cited by 1
- BoxIntegral.Box.subbox_induction_onproof · cited by 1
- BoxIntegral.Box.exists_mem_splitCenterBoxstatement and proof · cited by 0
- BoxIntegral.Box.iUnion_coe_splitCenterBoxstatement and proof · cited by 0