Connected

📁 Source: Mathlib/Topology/Separation/Connected.lean

Statistics

Metric	Count
Definitions	0
Theorems neBot_nhdsWithin_compl_of_nontrivial_of_t1space, infinite_of_nontrivial, infinite, trivial_of_discrete, t1Space	5
Total	5

ConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neBot_nhdsWithin_compl_of_nontrivial_of_t1space 📖	mathematical	—	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	nonempty_inter toPreconnectedSpace isOpen_compl_singleton isOpen_singleton_iff_punctured_nhds Filter.not_neBot Set.compl_union_self Set.nonempty_compl_of_nontrivial Set.singleton_nonempty Set.compl_inter_self

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite_of_nontrivial 📖	mathematical	IsPreconnected Set.Nontrivial	Set.Infinite	—	Set.subsingleton_coe PreconnectedSpace.trivial_of_discrete Subtype.preconnectedSpace Finite.instDiscreteTopology Subtype.t1Space Set.Finite.to_subtype Set.not_subsingleton_iff

PreconnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite 📖	mathematical	—	Infinite	—	Set.infinite_univ_iff IsPreconnected.infinite_of_nontrivial isPreconnected_univ Set.nontrivial_univ
trivial_of_discrete 📖	—	—	—	—	IsClopen.eq_univ isClopen_discrete Set.singleton_nonempty Set.mem_singleton_iff Set.mem_univ

TotallyDisconnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t1Space 📖	mathematical	—	T1Space	—	List.TFAE.out t1Space_TFAE totallyDisconnectedSpace_iff_connectedComponent_singleton isClosed_connectedComponent

---

← Back to Index