isBounded_pi_of_nonempty — Mathlib

English

If the pi-univ set is nonempty, then it is bounded if and only if each S_i is bounded.

Русский

Если множество pi-univ непусто, то оно ограничено тогда и только тогда, когда каждое S_i ограничено.

LaTeX

$$$( (\\pi\\,\\text{univ}\\,S).\\text{Nonempty} ) \\Rightarrow \\bigl( \\operatorname{IsBounded}(\\pi\\,\\text{univ}\\,S) \\iff \\forall i, \\operatorname{IsBounded}(S_i) \\bigr)$$$

Lean4

theorem isBounded_pi_of_nonempty (hne : (pi univ S).Nonempty) : IsBounded (pi univ S) ↔ ∀ i, IsBounded (S i) :=
  ⟨fun H i => @eval_image_univ_pi _ _ _ i hne ▸ forall_isBounded_image_eval_iff.2 H i, IsBounded.pi⟩

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