internlm/Lean-Github huggingface dataset:
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)
⊢ ∀ (a : P), IsCompact (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
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact (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)
a : P
⊢ IsCompact (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
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact ((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
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact ((fun a => closure (r '' Ici a)) a)
Tactic:
exact isClosed_closure.isCompact
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
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
⊢ {x | MapClusterPt x atTop r} = ⋂ a, s a
Tactic:
ext x
Proof state after:
case h
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)
x : X
⊢ x ∈ {x | MapClusterPt x atTop r} ↔ x ∈ ⋂ a, s a
Theorem: IsPreconnected.limits_atTop
Proof state before:
case h
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)
x : X
⊢ x ∈ {x | MapClusterPt x atTop r} ↔ x ∈ ⋂ a, s a
Tactic:
simp only [mem_setOf, mem_iInter, mapClusterPt_iff, mem_closure_iff_nhds, Set.Nonempty,
  @forall_comm P, ← hs]
Proof state after:
case h
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)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : P) in atTop, r a ∈ s) ↔ ∀ b ∈ 𝓝 x, ∀ (a : P), ∃ x, x ∈ b ∩ r '' Ici a
Theorem: IsPreconnected.limits_atTop
Proof state before:
case h
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)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : P) in atTop, r a ∈ s) ↔ ∀ b ∈ 𝓝 x, ∀ (a : P), ∃ x, x ∈ b ∩ r '' Ici a
Tactic:
apply forall_congr'
Proof state after:
case h.h
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)
x : X
⊢ ∀ (a : Set X), (a ∈ 𝓝 x → ∃ᶠ (a_2 : P) in atTop, r a_2 ∈ a) ↔ a ∈ 𝓝 x → ∀ (a_1 : P), ∃ x, x ∈ a ∩ r '' Ici a_1
Theorem: IsPreconnected.limits_atTop
Proof state before:
case h.h
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)
x : X
⊢ ∀ (a : Set X), (a ∈ 𝓝 x → ∃ᶠ (a_2 : P) in atTop, r a_2 ∈ a) ↔ a ∈ 𝓝 x → ∀ (a_1 : P), ∃ x, x ∈ a ∩ r '' Ici a_1
Tactic:
intro t
Proof state after:
case h.h
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)
x : X
t : Set X
⊢ (t ∈ 𝓝 x → ∃ᶠ (a : P) in atTop, r a ∈ t) ↔ t ∈ 𝓝 x → ∀ (a : P), ∃ x, x ∈ t ∩ r '' Ici a
Theorem: IsPreconnected.limits_atTop
Proof state before:
case h.h
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)
x : X
t : Set X
⊢ (t ∈ 𝓝 x → ∃ᶠ (a : P) in atTop, r a ∈ t) ↔ t ∈ 𝓝 x → ∀ (a : P), ∃ x, x ∈ t ∩ r '' Ici a
Tactic:
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:
no goals
Theorem: IsPreconnected.limits_atBot
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
rc : Continuous r
⊢ IsPreconnected {x | MapClusterPt x atBot r}
Tactic:
set r' : Pᵒᵈ → X := r
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Theorem: IsPreconnected.limits_atBot
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Tactic:
have rc' : Continuous r' := rc
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Theorem: IsPreconnected.limits_atBot
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Tactic:
have p' : ∀ a : Pᵒᵈ, IsPreconnected (Ici a) := fun a ↦ p 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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
p' : ∀ (a : Pᵒᵈ), IsPreconnected (Ici a)
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Theorem: IsPreconnected.limits_atBot
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
p' : ∀ (a : Pᵒᵈ), IsPreconnected (Ici a)
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Tactic:
exact IsPreconnected.limits_atTop p' rc'
Proof state after:
no goals
Theorem: IsPreconnected.limits_Ioc
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
by_cases ab : ¬a < b
Proof state after:
case pos
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
simp only [not_not] at ab
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
generalize hs : (fun t : Ioc a b ↦ closure (r '' Ioc a t)) = s
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have n : Nonempty (Ioc a b) := ⟨b, right_mem_Ioc.mpr ab⟩
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have m : Monotone s := by
  intro a b ab; rw [← hs]; refine closure_mono (monotone_image ?_)
  exact Ioc_subset_Ioc (le_refl _) (Subtype.coe_le_coe.mpr ab)
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have d : Directed Superset s := fun a b ↦ ⟨min a b, m (min_le_left _ _), m (min_le_right _ _)⟩
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have p : ∀ t, IsPreconnected (s t) := by
  intro ⟨t, m⟩; rw [← hs]; refine (isPreconnected_Ioc.image _ (rc.mono ?_)).closure
  simp only [mem_Ioc] at m
  simp only [Subtype.coe_mk, Ioc_subset_Ioc_iff m.1, m.2, le_refl, true_and_iff]
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have c : ∀ t, IsCompact (s t) := by intro t; rw [← hs]; exact isClosed_closure.isCompact
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
rw [e]
Proof state after:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
⊢ IsPreconnected (⋂ t, s t)
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case neg
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
⊢ IsPreconnected (⋂ t, s t)
Tactic:
exact IsPreconnected.directed_iInter d p c
Proof state after:
no goals
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case pos
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
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
simp only [Ioc_eq_empty ab, nhdsWithin_empty, MapClusterPt, Filter.map_bot, ClusterPt.bot,
  setOf_false, isPreconnected_empty]
Proof state after:
no goals