volume_real_Icc_of_le

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

English

If a ≤ b, then volume.real (Icc a b) = b - a.

Русский

Если a ≤ b, то volume.real(Icc a b) = b - a.

LaTeX

$$$\text{volume.real}(Icc(a,b)) = b - a$$$

Lean4

theorem volume_real_Icc_of_le {a b : ℝ} (hab : a ≤ b) : volume.real (Icc a b) = b - a := by simp [hab]

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

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

Разделы

Аффилиация

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