analysis icon indicating copy to clipboard operation
analysis copied to clipboard

use `patch` here?

Open affeldt-aist opened this issue 1 year ago • 0 comments

https://github.com/math-comp/analysis/blob/c518e2a302126cbc96a7527e28cac28aaf443822/theories/lebesgue_integral.v#L3420

i.e., f \_ D instead of f \* \1_ D ?

affeldt-aist avatar Nov 15 '23 13:11 affeldt-aist