Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 19:07 1db32c59

View on Github →

feat(set/basic): some results about set.pi (#3894) New definition: function.eval Also some changes in set.basic Name changes:

pi_empty_index -> empty_pi
pi_insert_index -> insert_pi
pi_singleton_index -> singleton_pi
set.push_pull -> image_inter_preimage
set.push_pull' -> image_preimage_inter

Estimated changes

added theorem set.empty_pi
added theorem set.eval_image_pi
added theorem set.eval_image_univ_pi
added theorem set.insert_pi
added theorem set.mem_pi
added theorem set.mem_univ_pi
modified def set.pi
deleted theorem set.pi_empty_index
added theorem set.pi_eq_empty
added theorem set.pi_eq_empty_iff
modified theorem set.pi_if
deleted theorem set.pi_insert_index
added theorem set.pi_nonempty_iff
deleted theorem set.pi_singleton_index
added theorem set.singleton_pi
added theorem set.univ_pi_eq_empty
added theorem set.update_preimage_pi
added def function.eval
added theorem function.eval_apply