α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent { val := x, property := h } else ∅)
α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
⊢ IsPreconnected (connectedComponentIn F x)
rw [connectedComponentIn]
case inl
α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
h✝ : x ∈ F
⊢ IsPreconnected (Subtype.val '' connectedComponent { val := x, property := h✝ })

case inr
α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
h✝ : ¬x ∈ F
⊢ IsPreconnected ∅
α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent { val := x, property := h } else ∅)
split_ifs
no goals
case inl
α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
h✝ : x ∈ F
⊢ IsPreconnected (Subtype.val '' connectedComponent { val := x, property := h✝ })
exact inducing_subtype_val.isPreconnected_image.mpr isPreconnected_connectedComponent
no goals
case inr
α : Type u
β : Type v
ι : Type ?u.53054
π : ι → Type ?u.53059
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
h✝ : ¬x ∈ F
⊢ IsPreconnected ∅
exact isPreconnected_empty