forall_isBounded_image_eval_iff — Mathlib

English

A set s is bounded if and only if all its coordinate images under eval i are bounded.

Русский

Множество s ограничено тогда и только тогда, когда все его координатные образы под eval_i ограничены.

LaTeX

$$$(\\forall i, \\operatorname{IsBounded}(\\mathrm{eval}_i''s)) \\iff \\operatorname{IsBounded}(s)$$$

Lean4

theorem forall_isBounded_image_eval_iff {s : Set (∀ i, X i)} : (∀ i, IsBounded (eval i '' s)) ↔ IsBounded s :=
  compl_mem_coprodᵢ.symm

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