Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-17 13:06 f33b0847

View on Github →

feat(topology/separation): generalize a lemma (#14154)

generalize nhds_eq_nhds_iff from a [t1_space α] to a [t0_space α];
relate indistinguishable to nhds.

Estimated changes

Modified src/topology/basic.lean

added theorem nhds_def'

Modified src/topology/separation.lean

modified theorem indistinguishable.eq

modified theorem indistinguishable_iff_closed

modified theorem indistinguishable_iff_closure

added theorem indistinguishable_iff_nhds_eq

modified theorem nhds_eq_nhds_iff