Def Set.graphOn

Modification history

2024-01-18 02:11

Mathlib/Data/Set/Defs.lean

chore(Data/Set): move definitions to a new file (#9737) …

Modified Set.graphOn View on Github →

2024-01-08 13:15

Mathlib/Data/Set/Function.lean

feat(Set/Function): define `Set.graphOn` (#9497) …

Added Set.graphOn View on Github →