Theorem: NontrivialAnalyticOn.isolated (Ray/AnalyticManifold/Nontrivial.lean)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
have fa : AnalyticAt ℂ (fun w ↦ f w - f z) z := (n.analyticOn z zs).sub analyticAt_const
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
cases' fa.eventually_eq_zero_or_eventually_ne_zero with h h
State after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 - f z ≠ 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

State before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
have b := h.and_frequently (n.nonconst z zs)
State after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
b : ∃ᶠ (x : ℂ) in 𝓝 z, f x - f z = 0 ∧ f x ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

State before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
b : ∃ᶠ (x : ℂ) in 𝓝 z, f x - f z = 0 ∧ f x ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
simp only [sub_eq_zero, Ne, and_not_self_iff, Filter.frequently_false] at b
State after:
no goals

State before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 - f z ≠ 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
simp only [sub_ne_zero] at h
State after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

State before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
exact h
State after:
no goals