α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
⊢ (preimage f^[n]) s =ᵐ[μ] s
α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
⊢ ∀ (n : ℕ), (preimage f^[n]) s =ᵐ[μ] s
intro n
case zero
α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
⊢ (preimage f^[Nat.zero]) s =ᵐ[μ] s

case succ
α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
ih : (preimage f^[n]) s =ᵐ[μ] s
⊢ (preimage f^[Nat.succ n]) s =ᵐ[μ] s
α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
⊢ (preimage f^[n]) s =ᵐ[μ] s
induction' n with n ih
no goals
case succ
α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
ih : (preimage f^[n]) s =ᵐ[μ] s
⊢ (preimage f^[Nat.succ n]) s =ᵐ[μ] s
simpa only [iterate_succ', comp_apply] using ae_eq_trans (hf.ae_eq ih) hs
no goals
case zero
α : Type u_1
β : Type ?u.495766
γ : Type ?u.495769
δ : Type ?u.495772
ι : Type ?u.495775
R : Type ?u.495778
R' : Type ?u.495781
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
f : α → α
hf : QuasiMeasurePreserving f
hs : f ⁻¹' s =ᵐ[μ] s
⊢ (preimage f^[Nat.zero]) s =ᵐ[μ] s
rfl