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