volume_uIoo — Mathlib

English

For x,y in the unit interval I, the volume of the symmetric open interval uIoo equals the distance edist(y,x).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem volume_uIoo : volume (uIoo x y) = edist y x := by
  simp only [uIoo, volume_apply, image_subtype_val_Ioo, Icc.coe_inf, Icc.coe_sup, Real.volume_Ioo, max_sub_min_eq_abs,
    edist_dist, Subtype.dist_eq, Real.dist_eq]

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