diam_pi_le_of_le — Mathlib

English

If every component s(b) has diameter ≤ c in the factors X(b), then the product set has diameter ≤ c.

Русский

Если каждый компонент s(b) имеет диаметр ≤ c в факторах X(b), то произведение имеет диаметр ≤ c.

LaTeX

$$\operatorname{diam}(\operatorname{Set.pi} \; univ\; s) \le c \,\text{ whenever } \forall b, \operatorname{diam}(s(b)) \le c$$

Lean4

theorem diam_pi_le_of_le {X : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (X b)] {s : ∀ b : β, Set (X b)} {c : ℝ≥0∞}
    (h : ∀ b, diam (s b) ≤ c) : diam (Set.pi univ s) ≤ c :=
  by
  refine diam_le fun x hx y hy => edist_pi_le_iff.mpr ?_
  rw [mem_univ_pi] at hx hy
  exact fun b => diam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)

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