image_eval

Mathlib.Topology.Bornology.Constructions

URI: https://scilib.ai/kg/mathlib#Bornology.IsBounded.image_eval

English

If s is bounded, then for every i, the image of s under eval i is bounded.

Русский

Если s ограничено, то для каждого i образ s под eval_i ограничен.

LaTeX

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

Lean4

theorem image_eval {s : Set (∀ i, X i)} (hs : IsBounded s) (i : ι) : IsBounded (eval i '' s) :=
  forall_isBounded_image_eval_iff.2 hs i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru