fst_of_prod

Mathlib.Topology.Bornology.Constructions

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

English

If s × t is bounded and t is nonempty, then s is bounded.

Русский

Если s × t ограничено и t непусто, то s ограничено.

LaTeX

$$$\forall s t,\ IsBounded(s\times t) \land t\neq \emptyset \Rightarrow IsBounded(s)$$$

Lean4

theorem fst_of_prod (h : IsBounded (s ×ˢ t)) (ht : t.Nonempty) : IsBounded s :=
  fst_image_prod s ht ▸ h.image_fst

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

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

Разделы

Аффилиация

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