Theorems · Theorem · measure theory
MeasurableEmbedding.exists_measurable_extend
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace γ] {f : α → β},
MeasurableEmbedding f → ∀ {g : α → γ}, Measurable g → (∀ (a : β), Nonempty γ) → ∃ g', Measurable g' ∧ g' ∘ f = g- Cited by
- 2 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- Measurablestatement and proof · cited by 1,499
- MeasurableEmbeddingstatement and proof · cited by 170
- Function.extendproof · cited by 111
- Function.Injective.extend_applyproof · cited by 57
- MeasurableEmbedding.injectiveproof · cited by 35
- measurable_const'proof · cited by 2
- MeasurableEmbedding.measurable_extendproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- MeasurableEmbedding.aemeasurable_map_iffproof · cited by 3
- MeasurableSet.exists_measurable_projproof · cited by 0