Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-15 09:41 0f287f82

View on Github →

chore(topology/separation): move/add simp lemmas (#16470)

  • add inseparable_iff_eq and inseparable_eq_eq;
  • add specializes_eq_eq, move @[simp] from specializes_iff_eq;
  • golf pure_le_nhds_iff and nhds_le_nhds_iff.

Estimated changes

added theorem inseparable_eq_eq
added theorem inseparable_iff_eq
added theorem specializes_eq_eq
modified theorem specializes_iff_eq