case intro.intro
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
⊢ IsPathConnected (Subtype.val ⁻¹' W)
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.648254
F U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (Subtype.val ⁻¹' W)
rcases hW with ⟨x, x_in, hx⟩
case intro.intro
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
⊢ ∀ {y : { x // x ∈ U }}, y ∈ Subtype.val ⁻¹' W → JoinedIn (Subtype.val ⁻¹' W) { val := x, property := (_ : x ∈ U) } y
case intro.intro
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
⊢ IsPathConnected (Subtype.val ⁻¹' W)
use ⟨x, hWU x_in⟩, by simp [x_in]
case intro.intro.mk
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
y : X
hyU : y ∈ U
hyW : { val := y, property := hyU } ∈ Subtype.val ⁻¹' W
⊢ JoinedIn (Subtype.val ⁻¹' W) { val := x, property := (_ : x ∈ U) } { val := y, property := hyU }
case intro.intro
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
⊢ ∀ {y : { x // x ∈ U }}, y ∈ Subtype.val ⁻¹' W → JoinedIn (Subtype.val ⁻¹' W) { val := x, property := (_ : x ∈ U) } y
rintro ⟨y, hyU⟩ hyW
no goals
case intro.intro.mk
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
y : X
hyU : y ∈ U
hyW : { val := y, property := hyU } ∈ Subtype.val ⁻¹' W
⊢ JoinedIn (Subtype.val ⁻¹' W) { val := x, property := (_ : x ∈ U) } { val := y, property := hyU }
exact ⟨(hx hyW).joined_subtype.somePath.map (continuous_inclusion hWU), by simp⟩
no goals
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
⊢ { val := x, property := (_ : x ∈ U) } ∈ Subtype.val ⁻¹' W
simp [x_in]
no goals
X : Type u_1
Y : Type ?u.648239
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.648254
F U W : Set X
hWU : W ⊆ U
x : X
x_in : x ∈ W
hx : ∀ {y : X}, y ∈ W → JoinedIn W x y
y : X
hyU : y ∈ U
hyW : { val := y, property := hyU } ∈ Subtype.val ⁻¹' W
⊢ ∀ (t : ↑I),
    ↑(Path.map
            (Joined.somePath
              (_ :
                Joined { val := x, property := (_ : x ∈ W) }
                  { val := ↑{ val := y, property := hyU }, property := (_ : ↑{ val := y, property := hyU } ∈ W) }))
            (_ : Continuous (inclusion hWU)))
        t ∈
      Subtype.val ⁻¹' W
simp