pi — Mathlib · SciLib

English

If every S_i is bounded, then the product set pi univ S is bounded.

Русский

Если каждый S_i ограничен, то множество произведения pi универсума S ограничено.

LaTeX

$$$(\\forall i, \\operatorname{IsBounded}(S_i)) \\Rightarrow \\operatorname{IsBounded}(\\pi\\,\\text{univ}\\,S)$$$

Lean4

theorem pi (h : ∀ i, IsBounded (S i)) : IsBounded (pi univ S) :=
  forall_isBounded_image_eval_iff.1 fun i => (h i).subset eval_image_univ_pi_subset

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