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