Theorems · Theorem · measure theory

MeasureTheory.MeasurePreserving.of_semiconj

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {ga : α → α} {gb : β → β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasureTheory.MeasurePreserving ga μa μa →
      Function.Semiconj f ga gb → Measurable gb → MeasureTheory.MeasurePreserving gb μb μb

Defined in: Mathlib.Dynamics.Ergodic.MeasurePreserving
Cited by: 1 results in Mathlib
Foundations: Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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
MeasureTheory.Measurestatement and proof · cited by 10,939
Measurablestatement and proof · cited by 1,499
MeasureTheory.Measure.mapproof · cited by 858
MeasureTheory.MeasurePreservingstatement and proof · cited by 259
Function.Semiconjstatement and proof · cited by 82
MeasureTheory.MeasurePreserving.map_eqproof · cited by 72
MeasureTheory.MeasurePreserving.compproof · cited by 40
MeasureTheory.MeasurePreserving.measurableproof · cited by 23
Function.Semiconj.comp_eqproof · cited by 11
MeasureTheory.MeasurePreserving.map_of_compproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconjproof · cited by 0