Theorems · Definition · general topology

connectedComponentIn

{α : Type u} → [TopologicalSpace α] → Set α → α → Set α

Given a set F in a topological space α and a point x : α, the connected component of x in F is the connected component of x in the subtype F seen as a set in α. This definition does not make sense if x is not in F so we return the empty set in this case.

Defined in

Mathlib.Topology.Connected.Basic

Cited by

33 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace