Theorem: IsPreconnected.nontrivialAnalyticOn (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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
⊢ ∀ x ∈ s, ∃ᶠ (y : ℂ) in 𝓝 x, f y ≠ f x
Tactic:
contrapose ne
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ¬∀ x ∈ s, ∃ᶠ (y : ℂ) in 𝓝 x, f y ≠ f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b

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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ¬∀ x ∈ s, ∃ᶠ (y : ℂ) in 𝓝 x, f y ≠ f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Tactic:
simp only [not_forall, Filter.not_frequently, not_not] at ne
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ∃ x, ∃ (_ : x ∈ s), ∀ᶠ (x_1 : ℂ) in 𝓝 x, f x_1 = f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b

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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
ne : ∃ x, ∃ (_ : x ∈ s), ∀ᶠ (x_1 : ℂ) in 𝓝 x, f x_1 = f x
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Tactic:
rcases ne with ⟨z, zs, h⟩
State after:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b

State before:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ¬∃ a b, a ∈ s ∧ b ∈ s ∧ f a ≠ f b
Tactic:
simp only [not_exists, exists_and_left, not_and, not_not]
State after:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1

State before:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Tactic:
have h' := (h.filter_mono (nhdsWithin_le_nhds (s := {z}ᶜ))).frequently
State after:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1

State before:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Tactic:
have e := fa.eqOn_of_preconnected_of_frequently_eq analyticOn_const p zs h'
State after:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1

State before:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1
Tactic:
intro x xs y ys
State after:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
x : ℂ
xs : x ∈ s
y : ℂ
ys : y ∈ s
⊢ f x = f y

State before:
case intro.intro
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 ℂ
p : IsPreconnected s
fa : AnalyticOn ℂ f s
z : ℂ
zs : z ∈ s
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
h' : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x = f z
e : EqOn f (fun x => f z) s
x : ℂ
xs : x ∈ s
y : ℂ
ys : y ∈ s
⊢ f x = f y
Tactic:
rw [e xs, e ys]
State after:
no goals