Commit 2022-09-27 17:24 33c6eeae

View on Github →

chore(topology/separation): rename separated to separated_nhds (#16604) E.g., Wikipedia uses "separated" for disjoint (closure s) t ∧ disjoint s (closure t).

Estimated changes

Modified src/topology/separation.lean

deleted theorem separated.comm

deleted theorem separated.disjoint_closure_left

deleted theorem separated.disjoint_closure_right

deleted theorem separated.empty_left

deleted theorem separated.empty_right

deleted theorem separated.mono

deleted theorem separated.preimage

deleted theorem separated.symm

deleted theorem separated.union_left

deleted theorem separated.union_right

deleted def separated

deleted theorem separated_iff_disjoint

added theorem separated_nhds.comm

added theorem separated_nhds.disjoint_closure_left

added theorem separated_nhds.disjoint_closure_right

added theorem separated_nhds.empty_left

added theorem separated_nhds.empty_right

added theorem separated_nhds.mono

added theorem separated_nhds.preimage

added theorem separated_nhds.symm

added theorem separated_nhds.union_left

added theorem separated_nhds.union_right

added def separated_nhds

added theorem separated_nhds_iff_disjoint