prod — Mathlib

English

If s is bounded and t is bounded, then their product s × t is bounded.

Русский

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

LaTeX

$$$(s \\text{ bounded}) \\land (t \\text{ bounded}) \\Rightarrow (s \\times t \\text{ bounded})$$$

Lean4

theorem prod (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ×ˢ t) :=
  isBounded_image_fst_and_snd.1 ⟨hs.subset <| fst_image_prod_subset _ _, ht.subset <| snd_image_prod_subset _ _⟩

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