Commit 2022-07-21 01:28 73cf56f1

View on Github →

feat(set_theory/zfc/basic): Set.mem_insert → Set.mem_insert_iff, add Set.mem_insert and Set.mem_insert_of_mem (#15573) The name Set.mem_insert_iff matches set.mem_insert_iff.

Estimated changes

Modified src/set_theory/zfc/basic.lean

modified theorem Set.mem_insert

added theorem Set.mem_insert_iff

added theorem Set.mem_insert_of_mem