case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
⊢ PathConnectedSpace X → IsPathConnected univ

case mpr
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
⊢ IsPathConnected univ → PathConnectedSpace X
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
⊢ PathConnectedSpace X ↔ IsPathConnected univ
constructor
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
⊢ IsPathConnected univ
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
⊢ PathConnectedSpace X → IsPathConnected univ
intro h
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
⊢ IsPathConnected univ
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
⊢ IsPathConnected univ
haveI := @PathConnectedSpace.Nonempty X _ _
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
inhabited_h : Inhabited X
⊢ IsPathConnected univ
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
⊢ IsPathConnected univ
inhabit X
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
inhabited_h : Inhabited X
⊢ ∀ {y : X}, y ∈ univ → JoinedIn univ default y
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
inhabited_h : Inhabited X
⊢ IsPathConnected univ
refine' ⟨default, mem_univ _, _⟩
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
inhabited_h : Inhabited X
y : X
_hy : y ∈ univ
⊢ JoinedIn univ default y
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
inhabited_h : Inhabited X
⊢ ∀ {y : X}, y ∈ univ → JoinedIn univ default y
intros y _hy
no goals
case mp
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.689194
F : Set X
h : PathConnectedSpace X
this : Nonempty X
inhabited_h : Inhabited X
y : X
_hy : y ∈ univ
⊢ JoinedIn univ default y
simpa using PathConnectedSpace.Joined default y
case mpr
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : IsPathConnected univ
⊢ PathConnectedSpace X
case mpr
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
⊢ IsPathConnected univ → PathConnectedSpace X
intro h
case mpr
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : IsPathConnected univ
h' : ∀ (x : X), x ∈ univ → ∀ (y : X), y ∈ univ → JoinedIn univ x y
⊢ PathConnectedSpace X
case mpr
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : IsPathConnected univ
⊢ PathConnectedSpace X
have h' := h.joinedIn
case mpr.intro
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.689194
F : Set X
h' : ∀ (x : X), x ∈ univ → ∀ (y : X), y ∈ univ → JoinedIn univ x y
x : X
h : x ∈ univ ∧ ∀ {y : X}, y ∈ univ → JoinedIn univ x y
⊢ PathConnectedSpace X
case mpr
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.689194
F : Set X
h : IsPathConnected univ
h' : ∀ (x : X), x ∈ univ → ∀ (y : X), y ∈ univ → JoinedIn univ x y
⊢ PathConnectedSpace X
cases' h with x h
no goals
case mpr.intro
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.689194
F : Set X
h' : ∀ (x : X), x ∈ univ → ∀ (y : X), y ∈ univ → JoinedIn univ x y
x : X
h : x ∈ univ ∧ ∀ {y : X}, y ∈ univ → JoinedIn univ x y
⊢ PathConnectedSpace X
exact ⟨⟨x⟩, by simpa using h'⟩
no goals
X : Type u_1
Y : Type ?u.689179
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.689194
F : Set X
h' : ∀ (x : X), x ∈ univ → ∀ (y : X), y ∈ univ → JoinedIn univ x y
x : X
h : x ∈ univ ∧ ∀ {y : X}, y ∈ univ → JoinedIn univ x y
⊢ ∀ (x y : X), Joined x y
simpa using h'