basic): `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` (#15573)

Commit

3 years ago

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`.

Author

vihdzp

Parents

bff41725

mathlib 73cf56f1 - feat(set_theory/zfc/basic): `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` (#15573)

mathlib
73cf56f1 - feat(set_theory/zfc/basic): `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` (#15573)