Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 11:25 c5e13baa

View on Github →

feat(algebra/order/pointwise): Supremum of pointwise operations (#13669) Pointwise operations of sets distribute over the (conditional) supremum/infimum.

Estimated changes

added theorem Inf_div
added theorem Inf_inv
added theorem Inf_mul
added theorem Inf_one
added theorem Sup_div
added theorem Sup_inv
added theorem Sup_mul
added theorem Sup_one
added theorem cInf_div
added theorem cInf_inv
added theorem cInf_mul
added theorem cInf_one
added theorem cSup_div
added theorem cSup_inv
added theorem cSup_mul
added theorem cSup_one