Def separated
Modification history
2022-09-27 17:24
src/topology/separation.lean
chore(topology/separation): rename `separated` to `separated_nhds` (#16604) …
Deleted separatedView on Github →2020-12-22 17:05
src/topology/separation.lean
feat(data/finset/basic, topology/separation): add induction_on_union, separate, and separate_finset_of_t2 (#5332) …
Added separatedView on Github →2020-06-24 06:13
src/topology/uniform_space/separation.lean
feat(uniform_space/separation): add separated_set (#3130) …
Deleted separatedView on Github →2019-03-05 14:15
src/topology/uniform_space/basic.lean
feat(topology): split uniform_space and topological_structure
Modified separatedView on Github →2018-01-19 16:18
analysis/topology/uniform_space.lean
feat(data/real,*): supporting material for metric spaces
Added separatedView on Github →