Commit 2024-01-08 13:15 869c0233
View on Github →feat(Set/Function): define Set.graphOn (#9497)
Also prove that s : Set (α × β) is a graph of a function on a set
if and only if Prod.fst is injective on s.
feat(Set/Function): define Set.graphOn (#9497)
Also prove that s : Set (α × β) is a graph of a function on a set
if and only if Prod.fst is injective on s.