Theorems · Theorem · measure theory
NNReal.summable_sigma
∀ {α : Type u_1} {β : α → Type u_4} {f : (x : α) × β x → NNReal},
Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩- Cited by
- 7 results in Mathlib
- Foundations
- Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- NNRealstatement and proof · cited by 4,310
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- ENNReal.ofNNRealproof · cited by 1,279
- NNReal.toRealproof · cited by 1,260
- tsumstatement and proof · cited by 1,148
- Summablestatement and proof · cited by 778
- ENNReal.coe_tsumproof · cited by 7
- NNReal.coe_tsumproof · cited by 6
- Summable.sigma_factorproof · cited by 3
- Summable.sigmaproof · cited by 2
- ENNReal.tsum_sigma'proof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- FormalMultilinearSeries.changeOriginSeries_summable_aux₁proof · cited by 3
- FormalMultilinearSeries.changeOriginSeries_summable_aux₂proof · cited by 3
- FormalMultilinearSeries.changeOrigin_radiusproof · cited by 3
- summable_sigma_of_nonnegproof · cited by 2
- FormalMultilinearSeries.comp_summable_nnrealproof · cited by 2
- FormalMultilinearSeries.changeOriginSeries_summable_aux₃proof · cited by 1
- FormalMultilinearSeries.nnnorm_changeOrigin_leproof · cited by 1