no goals
X : Type u_1
Y : Type ?u.563745
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.563760
F : Set X
h : JoinedIn F x y
⊢ Continuous fun t => { val := ↑(somePath h) t, property := (_ : ↑(somePath h) t ∈ F) }
continuity
no goals
X : Type u_1
Y : Type ?u.563745
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.563760
F : Set X
h : JoinedIn F x y
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => { val := ↑(somePath h) t, property := (_ : ↑(somePath h) t ∈ F) }) 0 =
    { val := x, property := (_ : x ∈ F) }
simp
no goals
X : Type u_1
Y : Type ?u.563745
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.563760
F : Set X
h : JoinedIn F x y
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => { val := ↑(somePath h) t, property := (_ : ↑(somePath h) t ∈ F) }) 1 =
    { val := y, property := (_ : y ∈ F) }
simp