Theorems · Theorem · real analysis
BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot
∀ {ι : Type u_1} [inst : Fintype ι] {c : NNReal} (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι)
(π₀ : BoxIntegral.Prepartition I),
π₀.distortion ≤ c → π₀.compl.distortion ≤ c → (l.toFilterDistortioniUnion I c π₀).NeBot- Cited by
- 0 results in Mathlib
- Foundations
- Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Fintypestatement and proof · cited by 7,736
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- NNRealstatement and proof · cited by 4,310
- Set.Ioiproof · cited by 1,463
- Filter.NeBotstatement · cited by 853
- BoxIntegral.Boxstatement and proof · cited by 464
- BoxIntegral.Prepartitionstatement and proof · cited by 199
- BoxIntegral.TaggedPrepartitionstatement and proof · cited by 126
- BoxIntegral.IntegrationParamsstatement and proof · cited by 101
- BoxIntegral.Prepartition.iUnionproof · cited by 71
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.