internlm/Lean-Github huggingface dataset:
Theorem: isClosed_closed_inter
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ closure (s ∩ u) ⊆ s
Tactic:
nth_rw 2 [← sc.closure_eq]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ closure (s ∩ u) ⊆ closure s
Theorem: isClosed_closed_inter
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ closure (s ∩ u) ⊆ closure s
Tactic:
apply closure_mono
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ s ∩ u ⊆ s
Theorem: isClosed_closed_inter
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ s ∩ u ⊆ s
Tactic:
apply inter_subset_left
Proof state after:
no goals
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
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
⊢ IsPreconnected s ↔ ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed sc]
Proof state after:
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
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
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
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
constructor
Proof state after:
case mp
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
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

case mpr
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
⊢ (∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp
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
⊢ (∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
intro h u v uo vo suv uv
Proof state after:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have suc : IsClosed (s ∩ u) := isClosed_closed_inter sc vo uv suv
Proof state after:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have svc : IsClosed (s ∩ v) := isClosed_closed_inter sc uo uv.symm ((union_comm u v).subst suv)
Proof state after:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have h0 : s ⊆ s ∩ u ∪ s ∩ v := by
  simp only [←inter_union_distrib_left]; exact subset_inter (subset_refl _) suv
Proof state after:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
have h1 : Disjoint (s ∩ u) (s ∩ v) := Disjoint.inter_left' _ (Disjoint.inter_right' _ uv)
Proof state after:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
cases' h (s ∩ u) (s ∩ v) suc svc h0 h1 with su sv
Proof state after:
case mp.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u ∨ s ⊆ v

case mp.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ s ∩ u ∪ s ∩ v
Tactic:
simp only [←inter_union_distrib_left]
Proof state after:
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ s ∩ (u ∪ v)
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
⊢ s ⊆ s ∩ (u ∪ v)
Tactic:
exact subset_inter (subset_refl _) suv
Proof state after:
no goals
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
left
Proof state after:
case mp.inl.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp.inl.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
su : s ⊆ s ∩ u
⊢ s ⊆ u
Tactic:
exact (subset_inter_iff.mp su).2
Proof state after:
no goals
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
right
Proof state after:
case mp.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mp.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), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set X
uo : IsOpen u
vo : IsOpen v
suv : s ⊆ u ∪ v
uv : Disjoint u v
suc : IsClosed (s ∩ u)
svc : IsClosed (s ∩ v)
h0 : s ⊆ s ∩ u ∪ s ∩ v
h1 : Disjoint (s ∩ u) (s ∩ v)
sv : s ⊆ s ∩ v
⊢ s ⊆ v
Tactic:
exact (subset_inter_iff.mp sv).2
Proof state after:
no goals
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr
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
⊢ (∀ (u v : Set X), IsOpen u → IsOpen v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v) →
    ∀ (u v : Set X), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Tactic:
intro h u v uc vc suv uv
Proof state after:
case mpr
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
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr
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
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
rcases NormalSpace.normal u v uc vc uv with ⟨u', v', uo, vo, uu, vv, uv'⟩
Proof state after:
case mpr.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
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'
⊢ s ⊆ u ∨ s ⊆ v
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.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
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'
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
cases' h u' v' uo vo (_root_.trans suv (union_subset_union uu vv)) uv' with h h
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.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'
⊢ s ⊆ u ∨ s ⊆ v

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
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.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'
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
left
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inl.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 ⊆ u'
⊢ s ⊆ u
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inl.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 ⊆ u'
⊢ s ⊆ u
Tactic:
intro x m
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.inl.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 ⊆ u'
x : X
m : x ∈ s
⊢ x ∈ u
Theorem: isPreconnected_iff_subset_of_fully_disjoint_open
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.inl.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 ⊆ u'
x : X
m : x ∈ s
⊢ x ∈ u
Tactic:
cases' (mem_union _ _ _).mp (suv m) with mu mv
Proof state after:
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