internlm/Lean-Github huggingface dataset:
Theorem: IsPreconnected.directed_iInter
Proof state before:
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 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
a : I
⊢ IsClosed (s a \ (u ∪ v))
Theorem: IsPreconnected.directed_iInter
Proof state before:
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
a : I
⊢ IsClosed (s a \ (u ∪ v))
Tactic:
exact ((c a).diff (uo.union vo)).isClosed
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)
h : ∀ (x : I), ∃ a ∈ s x, a ∉ u ∪ v
n : (⋂ a, s a \ (u ∪ v)).Nonempty
⊢ False
Tactic:
rcases n with ⟨x, n⟩
Proof state after:
case 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
x : X
n : x ∈ ⋂ a, s a \ (u ∪ v)
⊢ False
Theorem: IsPreconnected.directed_iInter
Proof state before:
case 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
x : X
n : x ∈ ⋂ a, s a \ (u ∪ v)
⊢ False
Tactic:
simp only [mem_iInter, mem_diff, forall_and, forall_const] at n
Proof state after:
case 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
x : X
n : (∀ (x_1 : I), x ∈ s x_1) ∧ x ∉ u ∪ v
⊢ False
Theorem: IsPreconnected.directed_iInter
Proof state before:
case 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
x : X
n : (∀ (x_1 : I), x ∈ s x_1) ∧ x ∉ u ∪ v
⊢ False
Tactic:
rw [← mem_iInter] at n
Proof state after:
case 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
x : X
n : x ∈ ⋂ i, s i ∧ x ∉ u ∪ v
⊢ False
Theorem: IsPreconnected.directed_iInter
Proof state before:
case 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
x : X
n : x ∈ ⋂ i, s i ∧ x ∉ u ∪ v
⊢ False
Tactic:
simp only [suv n.1, not_true, imp_false] at n
Proof state after:
case 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
x : X
n : x ∈ ⋂ i, s i ∧ False
⊢ False
Theorem: IsPreconnected.directed_iInter
Proof state before:
case 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
x : X
n : x ∈ ⋂ i, s i ∧ False
⊢ False
Tactic:
exact n.2
Proof state after:
no goals
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
generalize hs : (fun a ↦ closure (r '' Ici a)) = s
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have m : Antitone s := by
  intro a b ab; rw [← hs]; exact closure_mono (monotone_image (Ici_subset_Ici.mpr ab))
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have d : Directed Superset s := by
  intro a b; exact ⟨a ⊔ b, m le_sup_left, m le_sup_right⟩
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have p : ∀ a, IsPreconnected (s a) := by
  intro a; rw [← hs]; exact ((p _).image _ rc.continuousOn).closure
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have c : ∀ a, IsCompact (s a) := by
  intro a; rw [← hs]; exact isClosed_closure.isCompact
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have e : {x | MapClusterPt x atTop r} = ⋂ a, s a := by
  ext x
  simp only [mem_setOf, mem_iInter, mapClusterPt_iff, mem_closure_iff_nhds, Set.Nonempty,
    @forall_comm P, ← hs]
  apply forall_congr'; intro t
  simp only [@forall_comm P, mem_inter_iff, mem_image, mem_Ici, @and_comm (_ ∈ t),
    exists_exists_and_eq_and, Filter.frequently_atTop, exists_prop]
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
rw [e]
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected (⋂ a, s a)
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected (⋂ a, s a)
Tactic:
exact IsPreconnected.directed_iInter d p c
Proof state after:
no goals
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
⊢ Antitone s
Tactic:
intro a b ab
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ s b ≤ s a
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ s b ≤ s a
Tactic:
rw [← hs]
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ (fun a => closure (r '' Ici a)) b ≤ (fun a => closure (r '' Ici a)) a
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ (fun a => closure (r '' Ici a)) b ≤ (fun a => closure (r '' Ici a)) a
Tactic:
exact closure_mono (monotone_image (Ici_subset_Ici.mpr ab))
Proof state after:
no goals
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
⊢ Directed Superset s
Tactic:
intro a b
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
a b : P
⊢ ∃ z, s a ⊇ s z ∧ s b ⊇ s z
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
a b : P
⊢ ∃ z, s a ⊇ s z ∧ s b ⊇ s z
Tactic:
exact ⟨a ⊔ b, m le_sup_left, m le_sup_right⟩
Proof state after:
no goals
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
⊢ ∀ (a : P), IsPreconnected (s a)
Tactic:
intro a
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected (s a)
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected (s a)
Tactic:
rw [← hs]
Proof state after:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected ((fun a => closure (r '' Ici a)) a)
Theorem: IsPreconnected.limits_atTop
Proof state before:
X : Type
inst✝⁹ : TopologicalSpace X
I : Type
inst✝⁸ : TopologicalSpace I
inst✝⁷ : ConditionallyCompleteLinearOrder I
inst✝⁶ : DenselyOrdered I
inst✝⁵ : OrderTopology I
inst✝⁴ : CompactSpace X
inst✝³ : T4Space X
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected ((fun a => closure (r '' Ici a)) a)
Tactic:
exact ((p _).image _ rc.continuousOn).closure
Proof state after:
no goals