case intro
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x z
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z
cases' hxy.mem with hx hy
case intro.intro
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx✝ : x ∈ F
hy✝ hx : y ∈ F
hy : z ∈ F
⊢ JoinedIn F x z
case intro
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x z
cases' hyz.mem with hx hy
case intro.intro
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hx✝¹ : x ∈ F
hy✝¹ : y ∈ F
hy✝ : z ∈ F
hxy : Joined { val := x, property := (_ : x ∈ F) } { val := y, property := (_ : y ∈ F) }
hyz : Joined { val := y, property := (_ : y ∈ F) } { val := z, property := (_ : z ∈ F) }
hx✝ : x ∈ F
hx : y ∈ F
hy : z ∈ F
⊢ Joined { val := x, property := (_ : x ∈ F) } { val := z, property := (_ : z ∈ F) }
case intro.intro
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx✝ : x ∈ F
hy✝ hx : y ∈ F
hy : z ∈ F
⊢ JoinedIn F x z
simp_all [joinedIn_iff_joined]
no goals
case intro.intro
X : Type u_1
Y : Type ?u.622850
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.622865
F : Set X
hx✝¹ : x ∈ F
hy✝¹ : y ∈ F
hy✝ : z ∈ F
hxy : Joined { val := x, property := (_ : x ∈ F) } { val := y, property := (_ : y ∈ F) }
hyz : Joined { val := y, property := (_ : y ∈ F) } { val := z, property := (_ : z ∈ F) }
hx✝ : x ∈ F
hx : y ∈ F
hy : z ∈ F
⊢ Joined { val := x, property := (_ : x ∈ F) } { val := z, property := (_ : z ∈ F) }
exact hxy.trans hyz