α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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
⊢ limsup (compl ∘ fun n => (preimage f^[n]) s) atTop =ᵐ[μ] sᶜ
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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
⊢ liminf (fun n => (preimage f^[n]) s) atTop =ᵐ[μ] s
rw [← ae_eq_set_compl_compl, @Filter.liminf_compl (Set α)]
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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ᶜ
⊢ limsup (compl ∘ fun n => (preimage f^[n]) s) atTop =ᵐ[μ] sᶜ
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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
⊢ limsup (compl ∘ fun n => (preimage f^[n]) s) atTop =ᵐ[μ] sᶜ
rw [← ae_eq_set_compl_compl, ← preimage_compl] at hs
case h.e'_4.h.e'_4.h
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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ᶜ
x✝ : ℕ
⊢ (compl ∘ fun n => (preimage f^[n]) s) x✝ = (preimage f^[x✝]) (sᶜ)
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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ᶜ
⊢ limsup (compl ∘ fun n => (preimage f^[n]) s) atTop =ᵐ[μ] sᶜ
convert hf.limsup_preimage_iterate_ae_eq hs
case h.e'_4.h.e'_4.h.h
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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ᶜ
x✝ : ℕ
n : α
⊢ n ∈ (compl ∘ fun n => (preimage f^[n]) s) x✝ ↔ n ∈ (preimage f^[x✝]) (sᶜ)
case h.e'_4.h.e'_4.h
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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ᶜ
x✝ : ℕ
⊢ (compl ∘ fun n => (preimage f^[n]) s) x✝ = (preimage f^[x✝]) (sᶜ)
ext1 n
no goals
case h.e'_4.h.e'_4.h.h
α : Type u_1
β : Type ?u.496746
γ : Type ?u.496749
δ : Type ?u.496752
ι : Type ?u.496755
R : Type ?u.496758
R' : Type ?u.496761
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ᶜ
x✝ : ℕ
n : α
⊢ n ∈ (compl ∘ fun n => (preimage f^[n]) s) x✝ ↔ n ∈ (preimage f^[x✝]) (sᶜ)
simp only [← Set.preimage_iterate_eq, comp_apply, preimage_compl]