Mathlib Changelog
v3
Changelog
About
Github
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
Created
data/rel.lean
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.restrict_domain
added
def
rel
added
theorem
set.image_eq
added
theorem
set.preimage_eq
added
theorem
set.preimage_eq_core