internlm/Lean-Github huggingface dataset:
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)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
⊢ Monotone 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
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✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ s a ≤ s b
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✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ s a ≤ s b
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
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✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ (fun t => closure (r '' Ioc a✝ ↑t)) a ≤ (fun t => closure (r '' Ioc a✝ ↑t)) b
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✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ (fun t => closure (r '' Ioc a✝ ↑t)) a ≤ (fun t => closure (r '' Ioc a✝ ↑t)) b
Tactic:
refine closure_mono (monotone_image ?_)
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
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✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ Ioc a✝ ↑a ≤ Ioc a✝ ↑b
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✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ Ioc a✝ ↑a ≤ Ioc a✝ ↑b
Tactic:
exact Ioc_subset_Ioc (le_refl _) (Subtype.coe_le_coe.mpr ab)
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)
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
⊢ ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
Tactic:
intro ⟨t, m⟩
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
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
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected (s ⟨t, m⟩)
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)
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
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected (s ⟨t, m⟩)
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
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
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected ((fun t => closure (r '' Ioc a ↑t)) ⟨t, m⟩)
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)
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
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected ((fun t => closure (r '' Ioc a ↑t)) ⟨t, m⟩)
Tactic:
refine (isPreconnected_Ioc.image _ (rc.mono ?_)).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
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
t : ℝ
m : t ∈ Ioc a b
⊢ Ioc a ↑⟨t, m⟩ ⊆ Ioc a b
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)
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
t : ℝ
m : t ∈ Ioc a b
⊢ Ioc a ↑⟨t, m⟩ ⊆ Ioc a b
Tactic:
simp only [mem_Ioc] at m
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
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
t : ℝ
m✝ : t ∈ Ioc a b
m : a < t ∧ t ≤ b
⊢ Ioc a ↑⟨t, m✝⟩ ⊆ Ioc a b
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)
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
t : ℝ
m✝ : t ∈ Ioc a b
m : a < t ∧ t ≤ b
⊢ Ioc a ↑⟨t, m✝⟩ ⊆ Ioc a b
Tactic:
simp only [Subtype.coe_mk, Ioc_subset_Ioc_iff m.1, m.2, le_refl, true_and_iff]
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)
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)
⊢ ∀ (t : ↑(Ioc a b)), IsCompact (s t)
Tactic:
intro t
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
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)
t : ↑(Ioc a b)
⊢ IsCompact (s t)
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)
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)
t : ↑(Ioc a b)
⊢ IsCompact (s t)
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
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)
t : ↑(Ioc a b)
⊢ IsCompact ((fun t => closure (r '' Ioc a ↑t)) t)
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)
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)
t : ↑(Ioc a b)
⊢ IsCompact ((fun t => closure (r '' Ioc a ↑t)) t)
Tactic:
exact isClosed_closure.isCompact
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)
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)
⊢ {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
Tactic:
apply Set.ext
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
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)
⊢ ∀ (x : X), x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t
Theorem: IsPreconnected.limits_Ioc
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
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)
⊢ ∀ (x : X), x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t
Tactic:
intro 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
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)
x : X
⊢ x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t
Theorem: IsPreconnected.limits_Ioc
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
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)
x : X
⊢ x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t
Tactic:
simp only [mem_setOf, mem_iInter, mapClusterPt_iff, mem_closure_iff_nhds, Set.Nonempty,
  @forall_comm _ (Set X), ← 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
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)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ s) ↔
    ∀ (b_1 : Set X) (a_1 : ↑(Ioc a b)), b_1 ∈ 𝓝 x → ∃ x, x ∈ b_1 ∩ r '' Ioc a ↑a_1
Theorem: IsPreconnected.limits_Ioc
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
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)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ s) ↔
    ∀ (b_1 : Set X) (a_1 : ↑(Ioc a b)), b_1 ∈ 𝓝 x → ∃ x, x ∈ b_1 ∩ r '' Ioc a ↑a_1
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
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)
x : X
⊢ ∀ (a_1 : Set X),
    (a_1 ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ a_1) ↔
      ∀ (a_2 : ↑(Ioc a b)), a_1 ∈ 𝓝 x → ∃ x, x ∈ a_1 ∩ r '' Ioc a ↑a_2
Theorem: IsPreconnected.limits_Ioc
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
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)
x : X
⊢ ∀ (a_1 : Set X),
    (a_1 ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ a_1) ↔
      ∀ (a_2 : ↑(Ioc a b)), a_1 ∈ 𝓝 x → ∃ x, x ∈ a_1 ∩ r '' Ioc a ↑a_2
Tactic:
intro u
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
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)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), u ∈ 𝓝 x → ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Theorem: IsPreconnected.limits_Ioc
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
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)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), u ∈ 𝓝 x → ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Tactic:
simp only [@forall_comm _ (u ∈ 𝓝 x)]
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
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)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ u ∈ 𝓝 x → ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Theorem: IsPreconnected.limits_Ioc
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
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)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ u ∈ 𝓝 x → ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Tactic:
apply forall_congr'
Proof state after:
case h.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
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)
x : X
u : Set X
⊢ u ∈ 𝓝 x → ((∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_2 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_2)
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.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
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)
x : X
u : Set X
⊢ u ∈ 𝓝 x → ((∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_2 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_2)
Tactic:
intro _
Proof state after:
case h.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
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)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.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
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)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Tactic:
simp only [mem_inter_iff, Filter.frequently_iff, nhdsWithin_Ioc_eq_nhdsWithin_Ioi ab]
Proof state after:
case h.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
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)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1