no goals
α : Type u
β : Type v
ι : Type ?u.54113
π : ι → Type ?u.54118
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F
simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
  and_true_iff]