Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-04 21:21 e36ae183

View on Github →

feat(data/set/prod): set.off_diag (#16803) Define the off-diagonal of a set, which is the set of pairs of points whose components are distinct.

Estimated changes

added theorem set.mem_off_diag
added def set.off_diag
added theorem set.off_diag_empty
added theorem set.off_diag_eq_empty
added theorem set.off_diag_insert
added theorem set.off_diag_inter
added theorem set.off_diag_mono
added theorem set.off_diag_nonempty
added theorem set.off_diag_singleton
added theorem set.off_diag_union
added theorem set.off_diag_univ