image_fst

Mathlib.Topology.Bornology.Constructions

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

English

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

Русский

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

LaTeX

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

Lean4

theorem image_fst {s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.fst '' s) :=
  (isBounded_image_fst_and_snd.2 hs).1

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

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

Разделы

Аффилиация

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