Commit 2025-07-31 13:50 3e0fffb2
View on Github →feat: lemmas on the volume on I applied to intervals (#27513)
instance : NoAtoms (volume : Measure I)(volume : Measure I) s = volume (Subtype.val '' s)(volume : Measure I) (Icc x y) = ENNReal.ofReal (y - x)(volume : Measure I) (Ico x y) = ENNReal.ofReal (y - x)(volume : Measure I) (Ioc x y) = ENNReal.ofReal (y - x)(volume : Measure I) (Ioo x y) = ENNReal.ofReal (y - x)(volume : Measure I) (Iic x) = ENNReal.ofReal x(volume : Measure I) (Ici x) = ENNReal.ofReal (1 - x)(volume : Measure I) (Iio x) = ENNReal.ofReal x(volume : Measure I) (Ioi x) = ENNReal.ofReal (1 - x)(volume : Measure I) (uIcc x y) = edist y x(volume : Measure I) (uIoc x y) = edist y x(volume : Measure I) (uIoo x y) = edist y x