volume_pi_le_diam_pow — Mathlib

English

For s ⊆ (ι → ℝ), vol(s) ≤ diam(s)^{card(ι)}.

Русский

Для любого s ⊆ (ι → ℝ) имеет место vol(s) ≤ diam(s)^{card(ι)}.

LaTeX

$$$$ \\mathrm{volume}(s) \\le \\mathrm{diam}(s)^{|\\iota|}. $$$$

Lean4

theorem volume_pi_le_diam_pow (s : Set (ι → ℝ)) : volume s ≤ EMetric.diam s ^ Fintype.card ι :=
  calc
    volume s ≤ ∏ i : ι, EMetric.diam (Function.eval i '' s) := volume_pi_le_prod_diam s
    _ ≤ ∏ _i : ι, (1 : ℝ≥0) * EMetric.diam s :=
      (Finset.prod_le_prod' fun i _ => (LipschitzWith.eval i).ediam_image_le s)
    _ = EMetric.diam s ^ Fintype.card ι := by simp only [ENNReal.coe_one, one_mul, Finset.prod_const, Fintype.card]

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