internlm/Lean-Github huggingface dataset:
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ Complex.abs (z - a) < r ∧ ¬z = a
Tactic:
simp only [← e, add_sub_cancel_left, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos s0,
  Complex.abs_exp_ofReal_mul_I, mul_one, sr, true_and_iff, add_right_eq_self, mul_eq_zero,
  Complex.exp_ne_zero, or_false_iff, Complex.ofReal_eq_zero]
Proof state after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ ¬s = 0
Theorem: IsPreconnected.ball_diff_center
Proof state before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ ¬s = 0
Tactic:
exact s0.ne'
Proof state after:
no goals
Theorem: Complex.nonseparating_singleton
Proof 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]
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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⟩
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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⟩
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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}ᶜ
Theorem: Complex.nonseparating_singleton
Proof 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]
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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]
Proof state after:
no goals
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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}ᶜ
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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}ᶜ
Theorem: Complex.nonseparating_singleton
Proof 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
Proof state after:
no goals
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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 ⊢
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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⟩
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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}
Proof 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})
Theorem: Complex.nonseparating_singleton
Proof 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⟩
Proof 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
Theorem: Complex.nonseparating_singleton
Proof 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) _
Proof state after:
no goals
Theorem: AnalyticManifold.nonseparating_singleton
Proof 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 : S
⊢ Nonseparating {a}
Tactic:
apply Nonseparating.complexManifold
Proof 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 : S
⊢ ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Theorem: AnalyticManifold.nonseparating_singleton
Proof 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 : S
⊢ ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
intro z
Proof 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 z : S
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Theorem: AnalyticManifold.nonseparating_singleton
Proof 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 z : S
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
by_cases az : a ∈ (extChartAt I z).source
Proof 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 z : S
az : a ∈ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})

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 z : S
az : a ∉ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Theorem: AnalyticManifold.nonseparating_singleton
Proof 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 z : S
az : a ∈ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
convert Complex.nonseparating_singleton (extChartAt I z a)
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = {↑(extChartAt I z) a}
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = {↑(extChartAt I z) a}
Tactic:
simp only [eq_singleton_iff_unique_mem, mem_inter_iff, PartialEquiv.map_source _ az, true_and_iff,
  mem_preimage, mem_singleton_iff, PartialEquiv.left_inv _ az, eq_self_iff_true]
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ ∀ (x : ℂ), x ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x = a → x = ↑(extChartAt I z) a
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ ∀ (x : ℂ), x ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x = a → x = ↑(extChartAt I z) a
Tactic:
intro x ⟨m, e⟩
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
e : ↑(extChartAt I z).symm x = a
⊢ x = ↑(extChartAt I z) a
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
e : ↑(extChartAt I z).symm x = a
⊢ x = ↑(extChartAt I z) a
Tactic:
simp only [← e, PartialEquiv.right_inv _ m]
Proof state after:
no goals
Theorem: AnalyticManifold.nonseparating_singleton
Proof 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 z : S
az : a ∉ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
convert Nonseparating.empty
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = ∅
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = ∅
Tactic:
simp only [eq_empty_iff_forall_not_mem, mem_inter_iff, mem_preimage, mem_singleton_iff, not_and]
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ ∀ x ∈ (extChartAt I z).target, ¬↑(extChartAt I z).symm x = a
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ ∀ x ∈ (extChartAt I z).target, ¬↑(extChartAt I z).symm x = a
Tactic:
intro x m
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
⊢ ¬↑(extChartAt I z).symm x = a
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
⊢ ¬↑(extChartAt I z).symm x = a
Tactic:
contrapose az
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ¬¬↑(extChartAt I z).symm x = a
⊢ ¬a ∉ (extChartAt I z).source
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ¬¬↑(extChartAt I z).symm x = a
⊢ ¬a ∉ (extChartAt I z).source
Tactic:
simp only [not_not] at az ⊢
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ a ∈ (extChartAt I z).source
Theorem: AnalyticManifold.nonseparating_singleton
Proof state before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ a ∈ (extChartAt I z).source
Tactic:
rw [← az]
Proof state after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ ↑(extChartAt I z).symm x ∈ (extChartAt I z).source