internlm/Lean-Github huggingface dataset:
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
⊢ (∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
Tactic:
constructor
Proof state after:
case h.h.h.mp
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_2 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_2

case h.h.h.mpr
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_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1) → ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mp
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_2 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_2
Tactic:
intro h ⟨t, m⟩
Proof state after:
case h.h.h.mp
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
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mp
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
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Tactic:
have tm : Ioc a t ∈ 𝓝[Ioi a] a := by
  apply Ioc_mem_nhdsWithin_Ioi
  simp only [mem_Ioc] at m; simp only [mem_Ico]; use le_refl _, m.1
Proof state after:
case h.h.h.mp
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
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mp
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
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Tactic:
rcases h tm with ⟨v, vm, vu⟩
Proof state after:
case h.h.h.mp.intro.intro
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
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
v : ℝ
vm : v ∈ Ioc a t
vu : r v ∈ u
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mp.intro.intro
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
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
v : ℝ
vm : v ∈ Ioc a t
vu : r v ∈ u
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Tactic:
exact ⟨r v, vu, mem_image_of_mem _ vm⟩
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 : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ Ioc a t ∈ 𝓝[>] a
Tactic:
apply Ioc_mem_nhdsWithin_Ioi
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
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ a ∈ Ico a 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
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ a ∈ Ico a t
Tactic:
simp only [mem_Ioc] at m
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
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ∈ Ico a 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
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ∈ Ico a t
Tactic:
simp only [mem_Ico]
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
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ≤ a ∧ a < 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
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ≤ a ∧ a < t
Tactic:
use le_refl _, m.1
Proof state after:
no goals
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr
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_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1) → ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
Tactic:
intro h v vm
Proof state after:
case h.h.h.mpr
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
rcases mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.mp vm with ⟨w, wa, wv⟩
Proof state after:
case h.h.h.mpr.intro.intro
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wa : w ∈ Ioi a
wv : Ioc a w ⊆ v
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr.intro.intro
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wa : w ∈ Ioi a
wv : Ioc a w ⊆ v
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
simp only [mem_Ioi] at wa
Proof state after:
case h.h.h.mpr.intro.intro
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr.intro.intro
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
have m : min w b ∈ Ioc a b := by simp only [mem_Ioc]; use lt_min wa ab, min_le_right _ _
Proof state after:
case h.h.h.mpr.intro.intro
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr.intro.intro
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
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
rcases h ⟨_, m⟩ with ⟨x, xu, rx⟩
Proof state after:
case h.h.h.mpr.intro.intro.intro.intro
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : x ∈ r '' Ioc a ↑⟨min w b, m⟩
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr.intro.intro.intro.intro
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : x ∈ r '' Ioc a ↑⟨min w b, m⟩
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
simp only [Subtype.coe_mk, mem_image, mem_Ioc, le_min_iff] at rx
Proof state after:
case h.h.h.mpr.intro.intro.intro.intro
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : ∃ x_1, (a < x_1 ∧ x_1 ≤ w ∧ x_1 ≤ b) ∧ r x_1 = x
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr.intro.intro.intro.intro
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : ∃ x_1, (a < x_1 ∧ x_1 ≤ w ∧ x_1 ≤ b) ∧ r x_1 = x
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
rcases rx with ⟨c, ⟨ac, cw, _⟩, cx⟩
Proof state after:
case h.h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ ∃ x ∈ v, r x ∈ u
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case h.h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
use c, wv (mem_Ioc.mpr ⟨ac, cw⟩)
Proof state after:
case right
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✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ r c ∈ u