internlm/Lean-Github huggingface dataset:
Theorem: Nonseparating.complexManifold
Proof state before:
case h.e'_5.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
e : (extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c = ↑(extChartAt I z).symm '' c
ee : ↑(extChartAt I z).symm = ↑(extChartAt' I z).symm
x : S
y : ℂ
yz : y ∈ (extChartAt I z).target
yt : ↑(extChartAt I z).symm y ∉ t
yx : ↑(extChartAt I z).symm y = x
right✝ : x ∈ (extChartAt I z).source
⊢ x ∉ t ∧ x ∈ (extChartAt I z).source
Tactic:
simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and_iff]
Proof state after:
no goals
Theorem: Nonseparating.complexManifold
Proof state before:
case h.refine_3
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
⊢ IsPreconnected ((extChartAt I z).source ∩ ↑(extChartAt I z) ⁻¹' c)
Tactic:
rw [e]
Proof state after:
case h.refine_3
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
⊢ IsPreconnected (↑(extChartAt I z).symm '' c)
Theorem: Nonseparating.complexManifold
Proof state before:
case h.refine_3
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
⊢ IsPreconnected (↑(extChartAt I z).symm '' c)
Tactic:
apply cp.image
Proof state after:
case h.refine_3.hf
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
⊢ ContinuousOn (↑(extChartAt I z).symm) c
Theorem: Nonseparating.complexManifold
Proof state before:
case h.refine_3.hf
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
⊢ ContinuousOn (↑(extChartAt I z).symm) c
Tactic:
apply (continuousOn_extChartAt_symm I z).mono
Proof state after:
case h.refine_3.hf
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 ⊆ (extChartAt I z).target
Theorem: Nonseparating.complexManifold
Proof state before:
case h.refine_3.hf
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 ⊆ (extChartAt I z).target
Tactic:
exact _root_.trans cs (_root_.trans (diff_subset _ _) (inter_subset_left _ _))
Proof state after:
no goals
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : IsPreconnected s
so : IsOpen s
ts : Nonseparating t
⊢ IsPreconnected (s \ t)
Tactic:
rw [isPreconnected_iff_subset_of_disjoint] at sc ⊢
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
⊢ ∀ (u v : Set X), IsOpen u → IsOpen v → s \ t ⊆ u ∪ v → s \ t ∩ (u ∩ v) = ∅ → s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
⊢ ∀ (u v : Set X), IsOpen u → IsOpen v → s \ t ⊆ u ∪ v → s \ t ∩ (u ∩ v) = ∅ → s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
intro u v uo vo suv duv
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
generalize hf : (fun u : Set X ↦ u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ y in 𝓝[tᶜ] x, y ∈ u}) = f
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
have mono : ∀ u, u ⊆ f u := by rw [← hf]; exact fun _ ↦ subset_union_left _ _
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
have mem : ∀ {x u c}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u := by
  intro x u c m xt cn cu; rw [← hf]; right; use m, xt
  simp only [Filter.eventually_iff, setOf_mem_eq]; exact Filter.mem_of_superset cn cu
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
have cover : s ⊆ f u ∪ f v := by
  intro x m
  by_cases xt : x ∉ t; exact union_subset_union (mono _) (mono _) (suv (mem_diff_of_mem m xt))
  simp only [not_not] at xt
  rcases ts.loc x s xt (so.mem_nhds m) with ⟨c, cst, cn, cp⟩
  have d := inter_subset_inter_left (u ∩ v) cst; rw [duv, subset_empty_iff] at d
  cases' isPreconnected_iff_subset_of_disjoint.mp cp u v uo vo (_root_.trans cst suv) d with cu cv
  exact subset_union_left _ _ (mem m xt cn cu)
  exact subset_union_right _ _ (mem m xt cn cv)
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
have fdiff : ∀ {u}, f u \ t ⊆ u := by
  intro u x m; simp only [mem_diff, mem_union, mem_setOf, ← hf] at m
  simp only [m.2, false_and_iff, and_false_iff, or_false_iff, not_false_iff, and_true_iff] at m
  exact 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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
have fnon : ∀ {x u}, IsOpen u → x ∈ f u → ∀ᶠ y in 𝓝[tᶜ] x, y ∈ u := by
  intro x u o m; simp only [mem_union, mem_setOf, ← hf] at m
  cases' m with xu m; exact (o.eventually_mem xu).filter_mono nhdsWithin_le_nhds; exact m.2.2
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
have disj : s ∩ (f u ∩ f v) = ∅ := by
  contrapose duv; simp only [← ne_eq, ← nonempty_iff_ne_empty] at duv ⊢
  rcases duv with ⟨x, m⟩; simp only [mem_inter_iff] at m
  have b := ((so.eventually_mem m.1).filter_mono nhdsWithin_le_nhds).and
    ((fnon uo m.2.1).and (fnon vo m.2.2))
  simp only [eventually_nhdsWithin_iff] at b
  rcases eventually_nhds_iff.mp b with ⟨n, h, no, xn⟩
  rcases ts.dense.exists_mem_open no ⟨_, xn⟩ with ⟨y, yt, yn⟩
  use y; simp only [mem_inter_iff, mem_diff, ← mem_compl_iff]; specialize h y yn yt
  exact ⟨⟨h.1,yt⟩,h.2.1,h.2.2⟩
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
disj : s ∩ (f u ∩ f v) = ∅
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Theorem: IsPreconnected.open_diff
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
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
disj : s ∩ (f u ∩ f v) = ∅
⊢ s \ t ⊆ u ∨ s \ t ⊆ v
Tactic:
cases' sc (f u) (f v) (fopen uo) (fopen vo) cover disj with su sv
Proof state after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
disj : s ∩ (f u ∩ f v) = ∅
su : s ⊆ f u
⊢ s \ t ⊆ u ∨ s \ t ⊆ v

case inr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
s t : Set X
sc : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
so : IsOpen s
ts : Nonseparating t
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s \ t ⊆ u ∪ v
duv : s \ t ∩ (u ∩ v) = ∅
f : Set X → Set X
hf : (fun u => u ∪ {x | x ∈ s ∧ x ∈ t ∧ ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u}) = f
mono : ∀ (u : Set X), u ⊆ f u
fopen : ∀ {u : Set X}, IsOpen u → IsOpen (f u)
mem : ∀ {x : X} {u c : Set X}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u
cover : s ⊆ f u ∪ f v
fdiff : ∀ {u : Set X}, f u \ t ⊆ u
fnon : ∀ {x : X} {u : Set X}, IsOpen u → x ∈ f u → ∀ᶠ (y : X) in 𝓝[tᶜ] x, y ∈ u
disj : s ∩ (f u ∩ f v) = ∅
sv : s ⊆ f v
⊢ s \ t ⊆ u ∨ s \ t ⊆ v