case h_fin
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (f ⁻¹' s) ≠ ⊤

α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
replace h_fin : μ (f ⁻¹' s) ≠ ∞
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
refine' hf.quasiErgodic.ae_empty_or_univ' hs _
no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm
no goals
case h_fin
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (f ⁻¹' s) ≠ ⊤
rwa [hf.measure_preimage hs]