Theorem: IsPathConnected.of_frontier
Proof state before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Tactic:
refine ⟨⟨⟨q,qc⟩,?_,?_⟩,?_⟩
Proof state after:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 0 = x

case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 1 = p ⟨t, m⟩

case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ ∀ (t_1 : ↑unitInterval),
    { toFun := q, continuous_toFun := qc, source' := ?neg.refine_1✝, target' := ?neg.refine_2✝ } t_1 ∈ f ⁻¹' s