Theorem SetRel.isSeparated_insert_of_notMem

Modification history

2025-10-29 00:35
Mathlib/Data/Rel/Separated.lean
feat: relation-separated sets (#23920) …
Added SetRel.isSeparated_insert_of_notMemView on Github →