volume_uIoc — Mathlib

English

In the unit interval, the volume of the uIoc set between x and y equals the distance edist(y, x).

Русский

В единичном промежутке объем множества uIoc(x, y) равен расстоянию edist(y, x).

LaTeX

$$$\operatorname{volume}(uIoc(x, y)) = \operatorname{edist}(y, x)$$$

Lean4

@[simp]
theorem volume_uIoc : volume (uIoc x y) = edist y x := by
  simp only [uIoc, volume_apply, image_subtype_val_Ioc, Icc.coe_inf, Icc.coe_sup, Real.volume_Ioc, max_sub_min_eq_abs,
    edist_dist, Subtype.dist_eq, Real.dist_eq]

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