X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ (Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y) ↔ PathConnectedSpace ↑F
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ IsPathConnected F ↔ PathConnectedSpace ↑F
rw [isPathConnected_iff]
case mp
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ (Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y) → PathConnectedSpace ↑F

case mpr
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ PathConnectedSpace ↑F → Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ (Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y) ↔ PathConnectedSpace ↑F
constructor
case mp.intro.intro
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
⊢ PathConnectedSpace ↑F
case mp
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ (Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y) → PathConnectedSpace ↑F
rintro ⟨⟨x, x_in⟩, h⟩
case mp.intro.intro
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
⊢ ∀ (x y : ↑F), Joined x y
case mp.intro.intro
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
⊢ PathConnectedSpace ↑F
refine' ⟨⟨⟨x, x_in⟩⟩, _⟩
case mp.intro.intro.mk.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
⊢ Joined { val := y, property := y_in } { val := z, property := z_in }
case mp.intro.intro
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
⊢ ∀ (x y : ↑F), Joined x y
rintro ⟨y, y_in⟩ ⟨z, z_in⟩
case mp.intro.intro.mk.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
H : JoinedIn F y z
⊢ Joined { val := y, property := y_in } { val := z, property := z_in }
case mp.intro.intro.mk.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
⊢ Joined { val := y, property := y_in } { val := z, property := z_in }
have H := h y y_in z z_in
no goals
case mp.intro.intro.mk.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
h : ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
H : JoinedIn F y z
⊢ Joined { val := y, property := y_in } { val := z, property := z_in }
rwa [joinedIn_iff_joined y_in z_in] at H
case mpr.mk.intro.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.688463
F : Set X
H : ∀ (x y : ↑F), Joined x y
x : X
x_in : x ∈ F
⊢ Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
case mpr
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.688463
F : Set X
⊢ PathConnectedSpace ↑F → Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
rintro ⟨⟨x, x_in⟩, H⟩
case mpr.mk.intro.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
H : ∀ (x y : ↑F), Joined x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
⊢ JoinedIn F y z
case mpr.mk.intro.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.688463
F : Set X
H : ∀ (x y : ↑F), Joined x y
x : X
x_in : x ∈ F
⊢ Set.Nonempty F ∧ ∀ (x : X), x ∈ F → ∀ (y : X), y ∈ F → JoinedIn F x y
refine' ⟨⟨x, x_in⟩, fun y y_in z z_in => _⟩
case mpr.mk.intro.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
H : ∀ (x y : ↑F), Joined x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
⊢ Joined { val := y, property := y_in } { val := z, property := z_in }
case mpr.mk.intro.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
H : ∀ (x y : ↑F), Joined x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
⊢ JoinedIn F y z
rw [joinedIn_iff_joined y_in z_in]
no goals
case mpr.mk.intro.mk
X : Type u_1
Y : Type ?u.688448
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z✝ : X
ι : Type ?u.688463
F : Set X
H : ∀ (x y : ↑F), Joined x y
x : X
x_in : x ∈ F
y : X
y_in : y ∈ F
z : X
z_in : z ∈ F
⊢ Joined { val := y, property := y_in } { val := z, property := z_in }
apply H