ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ i ∧ (f^[b]) a ∈ s
ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
simp only [frequently_atTop, @forall_swap (_ ∈ s), ae_all_iff]
ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ n ∧ (f^[b]) a ∈ s
ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ i ∧ (f^[b]) a ∈ s
intro n
case h
ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) a ∈ s) → a ∈ s → ∃ b, b ≥ n ∧ (f^[b]) a ∈ s
ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ n ∧ (f^[b]) a ∈ s
filter_upwards [measure_zero_iff_ae_nmem.1 (hf.measure_mem_forall_ge_image_not_mem_eq_zero hs n)]
no goals
case h
ι : Type ?u.63965
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) a ∈ s) → a ∈ s → ∃ b, b ≥ n ∧ (f^[b]) a ∈ s
simp