← Copula mathematical handbook

Full support of uniform measure on the closed unit interval

instance ProbabilityTheory.Copula.isOpenPosMeasure_unitInterval : MeasureTheory.volume.IsOpenPosMeasure

Every nonempty relatively open subset of the unit interval has positive volume.