volume_real_Ico_of_le

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

English

If a ≤ b, then the real volume of Ico a b equals b - a: volume.real (Ico a b) = b - a.

Русский

Если a ≤ b, то реальный объем Ico a b равен b - a.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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