Theorems · Theorem · dynamical systems

MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_semiconj

∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {β : Type u_2}
  {m' : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ μ' → PreErgodic f μ → ∀ {f' : β → β}, Function.Semiconj g f f' → PreErgodic f' μ'

Defined in

Mathlib.Dynamics.Ergodic.Ergodic

Cited by

2 results in Mathlib

Foundations

Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound