Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 8db042f0

View on Github →

feat(data/rel): galois_connection (image r) (core r)

Estimated changes

modified theorem rel.core_comp
added theorem rel.core_preimage_gc
added theorem rel.image_subset_iff
modified theorem rel.preimage_comp
modified def rel.restrict_domain
modified theorem set.preimage_eq