Commit 2022-07-22 04:29 98c62bd0

View on Github →

feat(data/set/prod): add theorems about λ x, (x, x) (#15604) From the sphere eversion project. Also swap LHS with RHS in set.diagonal_eq_range and rename it to set.range_diag.

Estimated changes

Modified src/data/set/prod.lean

added theorem set.diag_preimage_prod

added theorem set.diag_preimage_prod_sellf

deleted theorem set.diagonal_eq_range

added theorem set.range_diag