English
For any set s, the volume of s is at most the product of the diameters of its coordinate projections: vol(s) ≤ ∏_{i} diam (Function.eval i '' s).
Русский
Для множества s верно: объём mера не превосходит произведение диаметров его координатных проекций: vol(s) ≤ ∏ diam (Function.eval_i'' s).
LaTeX
$$$$ \\mathrm{volume}(s) \\le \\prod_{i: ι} \\mathrm{diam}(\\mathrm{Function.eval}_i'' s). $$$$
Lean4
theorem volume_pi_le_prod_diam (s : Set (ι → ℝ)) : volume s ≤ ∏ i : ι, EMetric.diam (Function.eval i '' s) :=
calc
volume s ≤ volume (pi univ fun i => closure (Function.eval i '' s)) :=
volume.mono <| Subset.trans (subset_pi_eval_image univ s) <| pi_mono fun _ _ => subset_closure
_ = ∏ i, volume (closure <| Function.eval i '' s) := (volume_pi_pi _)
_ ≤ ∏ i : ι, EMetric.diam (Function.eval i '' s) :=
Finset.prod_le_prod' fun _ _ => (volume_le_diam _).trans_eq (EMetric.diam_closure _)
