volume_interval

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

URI: https://scilib.ai/kg/mathlib#Real.volume_interval

English

For any a,b ∈ ℝ, the volume of the closed interval between a and b is the length |b−a|.

Русский

Для любых a,b ∈ ℝ, объем замкнутого интервала между a и b равен длине |b−a|.

LaTeX

$$$\operatorname{volume}(uIcc(a,b)) = |b - a|$$$

Lean4

@[simp]
theorem volume_interval {a b : ℝ} : volume (uIcc a b) = ofReal |b - a| := by
  rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru