convexBodyLT_convex — Mathlib

English

The convex body LT is convex, hence its volume is well-behaved under linear maps.

Русский

Выпуклость тела LT сохраняется при линейных отображениях, что гарантирует корректность объема.

LaTeX

$$$\text{Convex }(\text{convexBodyLT } K f).$$$

Lean4

theorem convexBodyLT_convex : Convex ℝ (convexBodyLT K f) :=
  Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => convex_ball _ _))

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