Commit 2023-11-02 14:15 7e9b515b

View on Github →

feat(Data/Rel): prove simple propositions about images, preimages and graphs of relations (#6559) Add lemmas about relation composition with top and bottom elements, conditions under which images under a relation form the whole codomain, and the equivalence between being a functional relation and representable by the graph of a function.

Estimated changes

added theorem Equiv.graph_inv
added theorem Function.graph_comp
added theorem Function.graph_def
added theorem Function.graph_id
added theorem Rel.comp_left_bot
added theorem Rel.comp_left_top
added theorem Rel.comp_right_bot
added theorem Rel.comp_right_top
added theorem Rel.image_bot
added theorem Rel.image_empty
added theorem Rel.image_inter_dom_eq
added theorem Rel.image_top
added theorem Rel.inv_bot
added theorem Rel.inv_top
added theorem Rel.preimage_bot
added theorem Rel.preimage_empty
added theorem Rel.preimage_inv
added theorem Rel.preimage_top
added theorem Relation.is_graph_iff