Theorems · Theorem · real analysis
BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top
∀ {ι : Type u_1} [inst : Fintype ι] {I J : BoxIntegral.Box ι} (l : BoxIntegral.IntegrationParams) (h : I ≤ J),
Filter.Tendsto (⇑(BoxIntegral.TaggedPrepartition.embedBox I J h)) (BoxIntegral.IntegrationParams.toFilteriUnion I ⊤)
(BoxIntegral.IntegrationParams.toFilteriUnion J (BoxIntegral.Prepartition.single J I h))- Cited by
- 1 results in Mathlib
- Foundations
- Depth 161 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.
Cites41
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
- Setproof · cited by 53,352
- Realproof · cited by 25,697
- Top.topstatement and proof · cited by 9,680
- Fintypestatement and proof · cited by 7,736
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- NNRealproof · cited by 4,310
- Filter.Tendstostatement and proof · cited by 3,814
- iSupproof · cited by 2,415
- Set.Ioiproof · cited by 1,463
- Function.Embeddingstatement · cited by 988
Cited by1
Results whose statement or proof uses this declaration.
- BoxIntegral.Integrable.to_subbox_auxproof · cited by 2