Commit 2022-12-22 20:13 682500f4

View on Github →

feat: port Data.Rel (#1134)

Estimated changes

added def Function.graph
added def Rel.codom
added theorem Rel.codom_inv
added def Rel.comp
added theorem Rel.comp_assoc
added theorem Rel.comp_left_id
added theorem Rel.comp_right_id
added def Rel.core
added theorem Rel.core_comp
added theorem Rel.core_id
added theorem Rel.core_inter
added theorem Rel.core_mono
added theorem Rel.core_subset
added theorem Rel.core_union
added theorem Rel.core_univ
added def Rel.dom
added theorem Rel.dom_inv
added theorem Rel.dom_mono
added theorem Rel.ext
added def Rel.image
added theorem Rel.image_comp
added theorem Rel.image_core_gc
added theorem Rel.image_id
added theorem Rel.image_inter
added theorem Rel.image_mono
added theorem Rel.image_subset
added theorem Rel.image_subset_iff
added theorem Rel.image_union
added theorem Rel.image_univ
added def Rel.inv
added theorem Rel.inv_comp
added theorem Rel.inv_def
added theorem Rel.inv_id
added theorem Rel.inv_inv
added theorem Rel.mem_core
added theorem Rel.mem_image
added theorem Rel.mem_preimage
added def Rel.preimage
added theorem Rel.preimage_comp
added theorem Rel.preimage_def
added theorem Rel.preimage_id
added theorem Rel.preimage_inter
added theorem Rel.preimage_mono
added theorem Rel.preimage_union
added theorem Rel.preimage_univ
added def Rel
added theorem Set.image_eq
added theorem Set.preimage_eq
added theorem Set.preimage_eq_core