internlm/Lean-Github huggingface dataset:
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
a : I
auv : s a ⊆ u ∪ v
no : ¬¬(s a ⊆ u ∨ s a ⊆ v)
⊢ ¬¬(⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v)
Tactic:
simp only [not_not] at 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
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
a : I
auv : s a ⊆ u ∪ v
no : s a ⊆ u ∨ s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
cases' no with su sv
Proof state after:
case h.inl
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
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

case h.inr
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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Theorem: IsPreconnected.directed_iInter
Proof state before:
case h.inl
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
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v

case h.inr
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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
left
Proof state after:
case h.inl.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
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u

case h.inr
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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Theorem: IsPreconnected.directed_iInter
Proof state before:
case h.inl.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
su : s a ⊆ u
⊢ ⋂ a, s a ⊆ u

case h.inr
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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
exact _root_.trans (iInter_subset _ _) su
Proof state after:
case h.inr
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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Theorem: IsPreconnected.directed_iInter
Proof state before:
case h.inr
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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ u ∨ ⋂ a, s a ⊆ v
Tactic:
right
Proof state after:
case h.inr.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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ v
Theorem: IsPreconnected.directed_iInter
Proof state before:
case h.inr.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
sv : s a ⊆ v
⊢ ⋂ a, s a ⊆ v
Tactic:
exact _root_.trans (iInter_subset _ _) sv
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
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, s a ⊆ u ∪ v
Tactic:
by_contra h
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)
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)
h : ¬∃ a, s a ⊆ u ∪ v
⊢ False
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)
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)
h : ¬∃ a, s a ⊆ u ∪ v
⊢ False
Tactic:
simp only [not_exists, Set.not_subset] at h
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)
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ False
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)
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ False
Tactic:
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
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)
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ (⋂ a, s a \ (u ∪ v)).Nonempty
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)
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ (⋂ a, s a \ (u ∪ v)).Nonempty
Tactic:
apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
Proof state after:
case htd
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => s i \ (u ∪ v)

case htn
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Theorem: IsPreconnected.directed_iInter
Proof state before:
case htn
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), (s i \ (u ∪ v)).Nonempty

case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
intro a
Proof state after:
case htn
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ (s a \ (u ∪ v)).Nonempty

case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Theorem: IsPreconnected.directed_iInter
Proof state before:
case htn.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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
x : X
xa : x ∈ s a
xuv : x ∉ u ∪ v
⊢ (s a \ (u ∪ v)).Nonempty

case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
exact ⟨x, mem_diff_of_mem xa xuv⟩
Proof state after:
case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Theorem: IsPreconnected.directed_iInter
Proof state before:
case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsCompact (s i \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
intro a
Proof state after:
case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ IsCompact (s a \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Theorem: IsPreconnected.directed_iInter
Proof state before:
case htc
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
a : I
⊢ IsCompact (s a \ (u ∪ v))

case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))
Tactic:
exact (c a).diff (uo.union vo)
Proof state after:
case htcl
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
⊢ ∀ (i : I), IsClosed (s i \ (u ∪ v))