Theorems · Theorem · real analysis

BoxIntegral.unitPartition.setFinite_index

∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] {s : Set (ι → ℝ)},
  MeasureTheory.NullMeasurableSet s MeasureTheory.volume →
    MeasureTheory.volume s ≠ ⊤ → {ν | ↑(BoxIntegral.unitPartition.box n ν) ⊆ s}.Finite

Defined in: Mathlib.Analysis.BoxIntegral.UnitPartition
Cited by: 0 results in Mathlib
Foundations: Depth 247 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NeZero Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites30

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 and proof · cited by 53,352
Realstatement and proof · cited by 25,697
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Top.topstatement and proof · cited by 9,680
Fintypestatement and proof · cited by 7,736
Set.ofPredstatement and proof · cited by 6,101
le_reflproof · cited by 2,061
Set.Finitestatement · cited by 1,814
Fintype.cardproof · cited by 1,386
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.