Mathlib v3 is deprecated. Go to Mathlib v4

Theorem symmetric_rel.eq

Modification history

2022-07-19 18:28

src/topology/uniform_space/basic.lean

chore(topology/uniform_space/basic): rename `symmetric_rel_inter` to `symmetric_rel.inter` (#15441) …

Added symmetric_rel.eq View on Github →