# σ-algebra of sets invariant under a self-map #

In this file we define MeasurableSpace.invariants (f : α → α) to be the σ-algebra of sets s : Set α such that

• s is measurable w.r.t. the canonical σ-algebra on α;
• and f ⁻ˢ' s = s.
def MeasurableSpace.invariants {α : Type u_1} [m : ] (f : αα) :

Given a self-map f : α → α, invariants f is the σ-algebra of measurable sets that are invariant under f.

A set s is (invariants f)-measurable iff it is meaurable w.r.t. the canonical σ-algebra on α and f ⁻¹' s = s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableSpace.measurableSet_invariants {α : Type u_1} [] {f : αα} {s : Set α} :
f ⁻¹' s = s

A set s is (invariants f)-measurable iff it is meaurable w.r.t. the canonical σ-algebra on α and f ⁻¹' s = s.

@[simp]
theorem MeasurableSpace.invariants_id {α : Type u_1} [] :
= inst✝
theorem MeasurableSpace.invariants_le {α : Type u_1} [] (f : αα) :
inst✝
theorem MeasurableSpace.inf_le_invariants_comp {α : Type u_1} [] (f : αα) (g : αα) :
theorem MeasurableSpace.le_invariants_iterate {α : Type u_1} [] (f : αα) (n : ) :
theorem MeasurableSpace.measurable_invariants_dom {α : Type u_1} [] {β : Type u_2} [] {f : αα} {g : αβ} :
∀ (s : Set β), g f ⁻¹' s = g ⁻¹' s
theorem MeasurableSpace.measurable_invariants_of_semiconj {α : Type u_1} [] {β : Type u_2} [] {fa : αα} {fb : ββ} {g : αβ} (hg : ) (hfg : Function.Semiconj g fa fb) :