Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-02-12 21:14
dd13f00a
View on Github →
feat(data/set/intervals/basic): 24 lemmas about membership of arithmetic operations (
#6202
)
Estimated changes
Modified
src/data/set/intervals/basic.lean
added
theorem
set.add_mem_Icc_iff_left
added
theorem
set.add_mem_Icc_iff_right
added
theorem
set.add_mem_Ico_iff_left
added
theorem
set.add_mem_Ico_iff_right
added
theorem
set.add_mem_Ioc_iff_left
added
theorem
set.add_mem_Ioc_iff_right
added
theorem
set.add_mem_Ioo_iff_left
added
theorem
set.add_mem_Ioo_iff_right
added
theorem
set.inv_mem_Icc_iff
added
theorem
set.inv_mem_Ico_iff
added
theorem
set.inv_mem_Ioc_iff
added
theorem
set.inv_mem_Ioo_iff
added
theorem
set.sub_mem_Icc_iff_left
added
theorem
set.sub_mem_Icc_iff_right
added
theorem
set.sub_mem_Ico_iff_left
added
theorem
set.sub_mem_Ico_iff_right
added
theorem
set.sub_mem_Ioc_iff_left
added
theorem
set.sub_mem_Ioc_iff_right
added
theorem
set.sub_mem_Ioo_iff_left
added
theorem
set.sub_mem_Ioo_iff_right