internlm/Lean-Github huggingface dataset:
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ u

case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u
Tactic:
exact mu
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ u
Tactic:
exfalso
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ False
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inl.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ u'
x : X
m : x ∈ s
mv : x ∈ v
⊢ False
Tactic:
exact disjoint_left.mp uv' (h m) (vv mv)
Proof state after:
no goals
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
right
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
⊢ s ⊆ v
Tactic:
intro x m
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
⊢ x ∈ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
⊢ x ∈ v
Tactic:
cases' (mem_union _ _ _).mp (suv m) with mu mv
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ v

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ x ∈ v

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Tactic:
exfalso
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ False

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inl
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mu : x ∈ u
⊢ False

case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Tactic:
exact disjoint_right.mp uv' (h m) (uu mu)
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inr.h.inr
X : Type
inst✝⁵ : TopologicalSpace X
I : Type
inst✝⁴ : TopologicalSpace I
inst✝³ : ConditionallyCompleteLinearOrder I
inst✝² : DenselyOrdered I
inst✝¹ : OrderTopology I
inst✝ : NormalSpace X
s : Set X
sc : IsClosed s
h✝ : ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uc : IsClosed u
vc : IsClosed v
suv : s ⊆ u ∪ v
uv : Disjoint u v
u' v' : Set X
uo : IsOpen u'
vo : IsOpen v'
uu : u ⊆ u'
vv : v ⊆ v'
uv' : Disjoint u' v'
h : s ⊆ v'
x : X
m : x ∈ s
mv : x ∈ v
⊢ x ∈ v
Tactic:
exact mv
Proof state after:
no goals
Theorem: IsPreconnected.directed_iInter
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
p : ∀ (a : I), IsPreconnected (s a)
c : ∀ (a : I), IsCompact (s a)
⊢ IsPreconnected (⋂ a, s a)
Tactic:
contrapose p
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Theorem: IsPreconnected.directed_iInter
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Tactic:
have ci : IsClosed (⋂ a, s a) := isClosed_iInter fun i ↦ (c i).isClosed
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
ci : IsClosed (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Theorem: IsPreconnected.directed_iInter
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
p : ¬IsPreconnected (⋂ a, s a)
ci : IsClosed (⋂ a, s a)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Tactic:
simp only [isPreconnected_iff_subset_of_fully_disjoint_open ci, not_forall] at p
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Theorem: IsPreconnected.directed_iInter
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ¬∀ (a : I), IsPreconnected (s a)
Tactic:
simp only [isPreconnected_iff_subset_of_fully_disjoint_open (c _).isClosed, not_forall]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Theorem: IsPreconnected.directed_iInter
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
p :
  ∃ x x_1,
    ∃ (_ : IsOpen x) (_ : IsOpen x_1) (_ : ⋂ a, s a ⊆ x ∪ x_1) (_ : Disjoint x x_1), ¬(⋂ a, s a ⊆ x ∨ ⋂ a, s a ⊆ x_1)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
rcases p with ⟨u, v, uo, vo, suv, uv, no⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Theorem: IsPreconnected.directed_iInter
Proof state before:
case intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
have e : ∃ a, s a ⊆ u ∪ v := by
  by_contra h; simp only [not_exists, Set.not_subset] at h
  suffices n : (⋂ a, s a \ (u ∪ v)).Nonempty by
    rcases n with ⟨x, n⟩; simp only [mem_iInter, mem_diff, forall_and, forall_const] at n
    rw [← mem_iInter] at n; simp only [suv n.1, not_true, imp_false] at n; exact n.2
  apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
  intro a b; rcases d a b with ⟨c, ac, bc⟩
  use c, diff_subset_diff_left ac, diff_subset_diff_left bc
  intro a; rcases h a with ⟨x, xa, xuv⟩; exact ⟨x, mem_diff_of_mem xa xuv⟩
  intro a; exact (c a).diff (uo.union vo)
  intro a; exact ((c a).diff (uo.union vo)).isClosed
Proof state after:
case intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
e : ∃ a, s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Theorem: IsPreconnected.directed_iInter
Proof state before:
case intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
e : ∃ a, s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
rcases e with ⟨a, auv⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Theorem: IsPreconnected.directed_iInter
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ∃ x x_1 x_2,
    ∃ (_ : IsOpen x_1) (_ : IsOpen x_2) (_ : s x ⊆ x_1 ∪ x_2) (_ : Disjoint x_1 x_2), ¬(s x ⊆ x_1 ∨ s x ⊆ x_2)
Tactic:
use a, u, v, uo, vo, auv, uv
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ¬(s a ⊆ u ∨ s a ⊆ v)
Theorem: IsPreconnected.directed_iInter
Proof state before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
no : ¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
a : I
auv : s a ⊆ u ∪ v
⊢ ¬(s a ⊆ u ∨ s a ⊆ v)
Tactic:
contrapose no
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I✝ : Type
inst✝⁵ : TopologicalSpace I✝
inst✝⁴ : ConditionallyCompleteLinearOrder I✝
inst✝³ : DenselyOrdered I✝
inst✝² : OrderTopology I✝
I : Type
s : I → Set X
inst✝¹ : Nonempty I
inst✝ : T4Space X
d : Directed Superset s
c : ∀ (a : I), IsCompact (s a)
ci : IsClosed (⋂ a, s a)
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : ⋂ a, s a ⊆ u ∪ v
uv : Disjoint u v
a : I
auv : s a ⊆ u ∪ v
no : ¬¬(s a ⊆ u ∨ s a ⊆ v)
⊢ ¬¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)