Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-04 16:47 50beef25

View on Github →

feat(data/set/basic): more lemmas about set.pi (#5603)

Estimated changes

Modified src/data/pi.lean

added theorem pi.one_def

Modified src/data/set/basic.lean

added theorem set.pi_congr

added theorem set.pi_inter_compl

added theorem set.pi_univ

added theorem set.pi_update_of_mem

added theorem set.pi_update_of_not_mem

added theorem set.singleton_pi'

added theorem set.union_pi

added theorem set.univ_pi_update

added theorem set.univ_pi_update_univ

Modified src/data/set/intervals/pi.lean

added theorem set.disjoint_pi_univ_Ioc_update_left_right

added theorem set.pi_univ_Ioc_update_left

added theorem set.pi_univ_Ioc_update_right

added theorem set.pi_univ_Ioc_update_union