Theorems · Definition · real analysis
BoxIntegral.unitPartition.admissibleIndex
{ι : Type u_1} → (n : ℕ) → [NeZero n] → [Fintype ι] → BoxIntegral.Box ι → Finset (ι → ℤ)For B : BoxIntegral.Box, the set of indices of unitPartition.box that are subsets of B.
This is a finite set. These boxes cover B if it has integral vertices, see
unitPartition.prepartition_isPartition.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 249 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- BoxIntegral.Boxstatement and proof · cited by 464
- Set.Finite.toFinsetproof · cited by 351
Cited by10
Results whose statement or proof uses this declaration.
- BoxIntegral.unitPartition.prepartitionproof · cited by 10
- BoxIntegral.unitPartition.prepartition_tagstatement and proof · cited by 4
- BoxIntegral.unitPartition.mem_prepartition_iffstatement and proof · cited by 4
- BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_boxstatement · cited by 2
- BoxIntegral.unitPartition.mem_prepartition_boxes_iffstatement · cited by 2
- BoxIntegral.unitPartition.prepartition_isSubordinateproof · cited by 1
- BoxIntegral.unitPartition.box_index_tag_eq_selfproof · cited by 1
- BoxIntegral.unitPartition.prepartition_isHenstockproof · cited by 1
- BoxIntegral.unitPartition.admissibleIndex.congr_simpstatement and proof · cited by 0
- BoxIntegral.unitPartition.mem_admissibleIndex_iffstatement · cited by 0