Theorems · Definition · measure theory

MeasurableEmbedding.invFun

{α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → {f : α → β} → [Nonempty α] → MeasurableEmbedding f → β → α

The left-inverse of a MeasurableEmbedding

Defined in: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Cited by: 3 results in Mathlib
Foundations: Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace MeasurableSpace Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
MeasurableSpacestatement and proof · cited by 13,106
Set.rangeproof · cited by 4,705
Nonempty.someproof · cited by 340
MeasurableEmbeddingstatement and proof · cited by 170
MeasurableEquiv.symmproof · cited by 155
MeasurableEmbedding.equivRangeproof · cited by 4

Cited by3

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.exists_measurable_map_eq_unitIntervalproof · cited by 1
MeasurableEmbedding.measurable_invFunstatement · cited by 1
MeasurableEmbedding.leftInverse_invFunstatement · cited by 1