case zero
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[Nat.zero] ⁻¹' s =ᵐ[μ] s

case succ
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[Nat.succ k] ⁻¹' s =ᵐ[μ] s
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
k : ℕ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[k] ⁻¹' s =ᵐ[μ] s
induction' k with k ih
case succ
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' (f^[k] ⁻¹' s) =ᵐ[μ] s
case succ
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[Nat.succ k] ⁻¹' s =ᵐ[μ] s
rw [iterate_succ, preimage_comp]
no goals
case succ
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' (f^[k] ⁻¹' s) =ᵐ[μ] s
exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs
no goals
case zero
α : Type u_1
β : Type ?u.411803
γ : Type ?u.411806
δ : Type ?u.411809
ι : Type ?u.411812
R : Type ?u.411815
R' : Type ?u.411818
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
s : Set α
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[Nat.zero] ⁻¹' s =ᵐ[μ] s
rfl