Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 09:01 849d2a41

View on Github →

feat(analysis/topology/topological_space): define T0 spaces, T4 spaces, connected and irreducible sets and components (#448)

Estimated changes

modified theorem closure_singleton
added theorem exists_irreducible
added theorem exists_mem_inter
added def is_clopen
added theorem is_clopen_compl
added theorem is_clopen_compl_iff
added theorem is_clopen_diff
added theorem is_clopen_empty
added theorem is_clopen_iff
added theorem is_clopen_inter
added theorem is_clopen_union
added theorem is_clopen_univ
modified theorem is_closed_imp
added def is_connected
added theorem is_connected_closure
added theorem is_connected_empty
added theorem is_connected_sUnion
added theorem is_connected_singleton
added theorem is_connected_union
added def is_irreducible
added theorem is_irreducible_closure
added theorem is_irreducible_empty
added theorem normal_separation