Theorems · Theorem · measure theory
EReal.measurable_of_real_prod
∀ {β : Type u_6} {γ : Type u_7} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : EReal × β → γ},
(Measurable fun p => f (↑p.1, p.2)) → (Measurable fun x => f (⊥, x)) → (Measurable fun x => f (⊤, x)) → Measurable f- Cited by
- 1 results in Mathlib
- Foundations
- Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- Top.topstatement and proof · cited by 9,680
- Bot.botstatement and proof · cited by 4,720
- Set.rangeproof · cited by 4,705
- Set.univproof · cited by 3,945
- SProd.sprodproof · cited by 1,750
- Measurablestatement and proof · cited by 1,499
- ERealstatement and proof · cited by 793
- Real.toERealstatement and proof · cited by 303
- Set.range_idproof · cited by 37
- Set.range_prodMapproof · cited by 19
Cited by1
Results whose statement or proof uses this declaration.
- EReal.measurable_of_real_realproof · cited by 0