Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-17 05:06 0f6c1f19

View on Github →

feat(order/conditionally_complete_lattice): conditional Inf of intervals (#7226) Some new simp lemmas for cInf/cSup of intervals. I tried to use the minimal possible assumptions that I could - some lemmas are therefore in the linear order section and others are just for lattices.

Estimated changes

added theorem cInf_Icc
added theorem cInf_Ico
added theorem cInf_Ioc
added theorem cInf_Ioi
added theorem cInf_Ioo
added theorem cSup_Icc
added theorem cSup_Ico
added theorem cSup_Iio
added theorem cSup_Ioc
added theorem cSup_Ioo