internlm/Lean-Github huggingface dataset:
Theorem: Nonseparating.complexManifold
Proof state before:
case intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ ∃ c ⊆ u \ t, c ∈ 𝓝[tᶜ] z ∧ IsPreconnected c
Tactic:
use(extChartAt I z).source ∩ extChartAt I z ⁻¹' c
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ⊆ u \ t ∧
    (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ∈ 𝓝[tᶜ] z ∧
      IsPreconnected ((extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c)
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
⊢ ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
Tactic:
simp only [mem_inter_iff, mem_extChartAt_target I z, true_and_iff, mem_preimage,
  PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt]
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Tactic:
apply Filter.inter_mem
Proof state after:
case hs
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ (extChartAt I z).target ∈ 𝓝 (↑(extChartAt I z) z)

case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Theorem: Nonseparating.complexManifold
Proof state before:
case hs
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ (extChartAt I z).target ∈ 𝓝 (↑(extChartAt I z) z)

case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Tactic:
exact (isOpen_extChartAt_target I z).mem_nhds (mem_extChartAt_target I z)
Proof state after:
case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Theorem: Nonseparating.complexManifold
Proof state before:
case ht
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
⊢ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
Tactic:
exact extChartAt_preimage_mem_nhds _ un
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
Tactic:
apply Set.ext
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ ∀ (x : S), x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
⊢ ∀ (x : S), x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c
Tactic:
intro x
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c ↔ x ∈ ↑(extChartAt I z).symm '' c
Tactic:
simp only [mem_inter_iff, mem_preimage, mem_image]
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c ↔ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c ↔ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Tactic:
constructor
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c → ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x

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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ (∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x) → x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
Theorem: Nonseparating.complexManifold
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c → ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Tactic:
intro ⟨xz, xc⟩
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Theorem: Nonseparating.complexManifold
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x
Tactic:
refine ⟨_, xc, ?_⟩
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) x) = x
Theorem: Nonseparating.complexManifold
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
xz : x ∈ (extChartAt I z).source
xc : ↑(extChartAt I z) x ∈ c
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) x) = x
Tactic:
simp only [PartialEquiv.left_inv _ xz]
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
⊢ (∃ x_1 ∈ c, ↑(extChartAt I z).symm x_1 = x) → x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
Tactic:
intro ⟨y, yc, yx⟩
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ x ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) x ∈ c
Tactic:
rw [← yx]
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Theorem: Nonseparating.complexManifold
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c
Tactic:
have xc := cs yc
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
t : Set S
h : ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
z : S
u : Set S
zt : z ∈ t
un : u ∈ 𝓝 z
m : ↑(extChartAt I z) z ∈ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t
n : (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u ∈ 𝓝 (↑(extChartAt I z) z)
c : Set ℂ
cs :
  c ⊆
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
cn : c ∈ 𝓝[((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)ᶜ] ↑(extChartAt I z) z
cp : IsPreconnected c
x : S
y : ℂ
yc : y ∈ c
yx : ↑(extChartAt I z).symm y = x
xc :
  y ∈
    ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' u) \ ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' t)
⊢ ↑(extChartAt I z).symm y ∈ (extChartAt I z).source ∧ ↑(extChartAt I z) (↑(extChartAt I z).symm y) ∈ c