Theorem: Complex.nonseparating_singleton (Ray/AnalyticManifold/Nonseparating.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
⊢ Dense {a}ᶜ
Tactic:
rw [dense_iff_inter_open]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
⊢ ∀ (U : Set ℂ), IsOpen U → U.Nonempty → (U ∩ {a}ᶜ).Nonempty

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
⊢ ∀ (U : Set ℂ), IsOpen U → U.Nonempty → (U ∩ {a}ᶜ).Nonempty
Tactic:
intro u uo ⟨z, m⟩
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
⊢ (u ∩ {a}ᶜ).Nonempty

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
by_cases za : z ≠ a
State after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z ≠ a
⊢ (u ∩ {a}ᶜ).Nonempty

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : ¬z ≠ a
⊢ (u ∩ {a}ᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : ¬z ≠ a
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
simp only [not_not] at za
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z = a
⊢ (u ∩ {a}ᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z = a
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
rw [za] at m
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : a ∈ u
za : z = a
⊢ (u ∩ {a}ᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : a ∈ u
za : z = a
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
clear za z
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
⊢ (u ∩ {a}ᶜ).Nonempty

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
rcases Metric.isOpen_iff.mp uo a m with ⟨r, rp, rs⟩
State after:
case neg.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ (u ∩ {a}ᶜ).Nonempty

State before:
case neg.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
use a + r / 2
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ a + ↑r / 2 ∈ u ∩ {a}ᶜ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ a + ↑r / 2 ∈ u ∩ {a}ᶜ
Tactic:
simp only [mem_inter_iff, mem_compl_iff, mem_singleton_iff, add_right_eq_self,
  div_eq_zero_iff, Complex.ofReal_eq_zero, bit0_eq_zero, one_ne_zero, or_false_iff,
  rp.ne', not_false_iff, and_true_iff, false_or, two_ne_zero]
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ a + ↑r / 2 ∈ u

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ a + ↑r / 2 ∈ u
Tactic:
apply rs
State after:
case h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ a + ↑r / 2 ∈ ball a r

State before:
case h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
m : a ∈ u
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ a + ↑r / 2 ∈ ball a r
Tactic:
simp only [mem_ball, dist_self_add_left, Complex.norm_eq_abs, map_div₀, Complex.abs_ofReal,
  Complex.abs_two, abs_of_pos rp, half_lt_self rp]
State after:
no goals

State before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z ≠ a
⊢ (u ∩ {a}ᶜ).Nonempty
Tactic:
use z
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z ≠ a
⊢ z ∈ u ∩ {a}ᶜ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z ≠ a
⊢ z ∈ u ∩ {a}ᶜ
Tactic:
use m
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z ≠ a
⊢ z ∈ {a}ᶜ

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
uo : IsOpen u
z : ℂ
m : z ∈ u
za : z ≠ a
⊢ z ∈ {a}ᶜ
Tactic:
exact za
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
⊢ ∀ (x : ℂ) (u : Set ℂ), x ∈ {a} → u ∈ 𝓝 x → ∃ c ⊆ u \ {a}, c ∈ 𝓝[{a}ᶜ] x ∧ IsPreconnected c
Tactic:
intro z u m n
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : ℂ
u : Set ℂ
m : z ∈ {a}
n : u ∈ 𝓝 z
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[{a}ᶜ] z ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : ℂ
u : Set ℂ
m : z ∈ {a}
n : u ∈ 𝓝 z
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[{a}ᶜ] z ∧ IsPreconnected c
Tactic:
simp only [mem_singleton_iff] at m
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : ℂ
u : Set ℂ
n : u ∈ 𝓝 z
m : z = a
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[{a}ᶜ] z ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : ℂ
u : Set ℂ
n : u ∈ 𝓝 z
m : z = a
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[{a}ᶜ] z ∧ IsPreconnected c
Tactic:
simp only [m] at n ⊢
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : ℂ
u : Set ℂ
m : z = a
n : u ∈ 𝓝 a
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[≠] a ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : ℂ
u : Set ℂ
m : z = a
n : u ∈ 𝓝 a
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[≠] a ∧ IsPreconnected c
Tactic:
clear m z
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[≠] a ∧ IsPreconnected c

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[≠] a ∧ IsPreconnected c
Tactic:
rcases Metric.mem_nhds_iff.mp n with ⟨r, rp, rs⟩
State after:
case intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[≠] a ∧ IsPreconnected c

State before:
case intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ ∃ c ⊆ u \ {a}, c ∈ 𝓝[≠] a ∧ IsPreconnected c
Tactic:
use ball a r \ {a}
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ ball a r \ {a} ⊆ u \ {a} ∧ ball a r \ {a} ∈ 𝓝[≠] a ∧ IsPreconnected (ball a r \ {a})

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ ball a r \ {a} ⊆ u \ {a} ∧ ball a r \ {a} ∈ 𝓝[≠] a ∧ IsPreconnected (ball a r \ {a})
Tactic:
refine ⟨diff_subset_diff_left rs, ?_, IsPreconnected.ball_diff_center⟩
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ ball a r \ {a} ∈ 𝓝[≠] a

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
u : Set ℂ
n : u ∈ 𝓝 a
r : ℝ
rp : r > 0
rs : ball a r ⊆ u
⊢ ball a r \ {a} ∈ 𝓝[≠] a
Tactic:
exact diff_mem_nhdsWithin_compl (Metric.ball_mem_nhds _ rp) _
State after:
no goals