ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
have : ∀ s ∈ countableBasis α, ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, (f^[n]) x ∈ s := fun s hs =>
  h.ae_mem_imp_frequently_image_mem (isOpen_of_mem_countableBasis hs).measurableSet
ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
refine' ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => _
case intro.intro.intro
ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ i
s : Set α
hs : s ∈ 𝓝 x
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
rcases (isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩
no goals
case intro.intro.intro
ι : Type ?u.76491
α : Type u_1
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ i
s : Set α
hs : s ∈ 𝓝 x
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
exact (hx o hoS hxo).mono fun n hn => hos hn