image_snd

Mathlib.Topology.Bornology.Constructions

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

English

If s is bounded, then its projection to β is bounded.

Русский

Если s ограничено, то его проекция на β ограничена.

LaTeX

$$$\operatorname{IsBounded}(s) \Rightarrow \operatorname{IsBounded}(\operatorname{Prod.snd}''s)$$$

Lean4

theorem image_snd {s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.snd '' s) :=
  (isBounded_image_fst_and_snd.2 hs).2

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

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

Разделы

Аффилиация

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