case intro.intro
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ IsPathConnected (U ∪ V)
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : Set.Nonempty (U ∩ V)
⊢ IsPathConnected (U ∪ V)
rcases hUV with ⟨x, xU, xV⟩
case intro.intro
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ ∀ {y : X}, y ∈ U ∪ V → JoinedIn (U ∪ V) x y
case intro.intro
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ IsPathConnected (U ∪ V)
use x, Or.inl xU
case intro.intro.inl
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

case intro.intro.inr
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y
case intro.intro
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ ∀ {y : X}, y ∈ U ∪ V → JoinedIn (U ∪ V) x y
rintro y (yU | yV)
no goals
case intro.intro.inl
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y
exact (hU.joinedIn x xU y yU).mono (subset_union_left U V)
no goals
case intro.intro.inr
X : Type u_1
Y : Type ?u.646605
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.646620
F U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y
exact (hV.joinedIn x xV y yV).mono (subset_union_right U V)