volume_uIcc — Mathlib

English

For x,y in the unit interval I, the volume of the symmetric closed interval between x and y, denoted uIcc, equals the distance edist(y,x).

Русский

Для x,y из единичного интервала I мера симметричного замкнутого интервала между x и y равна расстоянию edist(y,x).

LaTeX

$$$\forall x,y \in I,\; \operatorname{vol}(\mathrm{uIcc}(x,y)) = \operatorname{edist}(y,x).$$$

Lean4

@[simp]
theorem volume_uIcc : volume (uIcc x y) = edist y x := by
  simp only [uIcc, volume_apply, image_subtype_val_Icc, Icc.coe_inf, Icc.coe_sup, Real.volume_Icc, max_sub_min_eq_abs,
    edist_dist, Subtype.dist_eq, Real.dist_eq]

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