convexBodySum_volume_eq_zero_of_le_zero

English

If B ≤ 0, then the volume of convexBodySum K B is zero.

Русский

Если B ≤ 0, то объём convexBodySum K B равен нулю.

LaTeX

$$\$ B \\le 0 \\implies \\operatorname{volume}(\\mathrm{convexBodySum}\\,K\\,B) = 0 \$$$

Lean4

theorem convexBodySum_volume_eq_zero_of_le_zero {B} (hB : B ≤ 0) : volume (convexBodySum K B) = 0 :=
  by
  obtain hB | hB := lt_or_eq_of_le hB
  · suffices convexBodySum K B = ∅ by rw [this, measure_empty]
    ext x
    refine ⟨fun hx => ?_, fun h => h.elim⟩
    rw [Set.mem_setOf] at hx
    linarith [convexBodySumFun_nonneg x]
  · suffices convexBodySum K B = {0} by rw [this, measure_singleton]
    ext
    rw [convexBodySum, Set.mem_setOf_eq, Set.mem_singleton_iff, hB, ← convexBodySumFun_eq_zero_iff]
    exact (convexBodySumFun_nonneg _).ge_iff_eq'

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