Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 4779af77

View on Github →

feat(data/rel): a type for binary relations

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_union
added theorem rel.core_univ
added def rel.dom
added theorem rel.dom_inv
added def rel.image
added theorem rel.image_comp
added theorem rel.image_id
added theorem rel.image_inter
added theorem rel.image_mono
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