snd_of_prod — Mathlib

English

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

Русский

Если произведение множеств s × t ограничено и множество s непусто, то множество t ограничено.

LaTeX

$$$\\text{If } (s \\times t) \\text{ is bounded and } s \\neq \\varnothing, \\text{ then } t \\text{ is bounded.}$$$

Lean4

theorem snd_of_prod (h : IsBounded (s ×ˢ t)) (hs : s.Nonempty) : IsBounded t :=
  snd_image_prod hs t ▸ h.image_snd

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