Theorem: IsPreconnected.directed_iInter
Proof state before:
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
a b : I
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) a) ((fun i => s i \ (u ∪ v)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) b) ((fun i => s i \ (u ∪ v)) z)

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:
rcases d a b with ⟨c, ac, bc⟩
Proof state after:
case htd.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 b c : I
ac : s a ⊇ s c
bc : s b ⊇ s c
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) a) ((fun i => s i \ (u ∪ v)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => s i \ (u ∪ v)) b) ((fun i => s i \ (u ∪ v)) z)

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))