instMeasureSpaceElemReal — Mathlib

English

The unit interval I carries a canonical measure-space structure, inherited from its embedding into the real line.

Русский

Единичный интервал I имеет каноническую структуру пространства меры, наследуемую от встраивания в действительную прямую.

LaTeX

$$$\text{unitInterval is endowed with a measure space structure via its embedding into } \mathbb{R}$$$

Lean4

noncomputable instance : MeasureSpace I :=
  Measure.Subtype.measureSpace

Похожие утверждения