case intro.intro
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x✝ y z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ IsPathConnected (f '' F)
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x y z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
hF : IsPathConnected F
f : X → Y
hf : Continuous f
⊢ IsPathConnected (f '' F)
rcases hF with ⟨x, x_in, hx⟩
case intro.intro
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x✝ y z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ ∀ {y : Y}, y ∈ f '' F → JoinedIn (f '' F) (f x) y
case intro.intro
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x✝ y z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ IsPathConnected (f '' F)
use f x, mem_image_of_mem f x_in
case intro.intro.intro.intro
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x✝ y✝ z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y)
case intro.intro
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x✝ y z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ ∀ {y : Y}, y ∈ f '' F → JoinedIn (f '' F) (f x) y
rintro _ ⟨y, y_in, rfl⟩
no goals
case intro.intro.intro.intro
X : Type u_2
Y✝ : Type ?u.644326
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x✝ y✝ z : X
ι : Type ?u.644341
F : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y)
exact ⟨(hx y_in).somePath.map hf, fun t => ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩