α : Type u
β : Type v
ι : Type ?u.51675
π : ι → Type ?u.51680
inst✝ : TopologicalSpace α
s t u v F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent { val := x, property := h } else ∅) ⊆ F
α : Type u
β : Type v
ι : Type ?u.51675
π : ι → Type ?u.51680
inst✝ : TopologicalSpace α
s t u v F : Set α
x : α
⊢ connectedComponentIn F x ⊆ F
rw [connectedComponentIn]
no goals
α : Type u
β : Type v
ι : Type ?u.51675
π : ι → Type ?u.51680
inst✝ : TopologicalSpace α
s t u v F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent { val := x, property := h } else ∅) ⊆ F
split_ifs <;> simp