isBounded_mul — Mathlib

English

If s,t are bounded subsets of a ring R with a bounded multiplication, then s·t is bounded.

Русский

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

LaTeX

$$$\forall s,t\subseteq R,\ IsBounded(s) \land IsBounded(t) \Rightarrow IsBounded(s\cdot t)$$$

Lean4

@[to_additive]
theorem isBounded_mul [Bornology R] [Mul R] [BoundedMul R] {s t : Set R} (hs : Bornology.IsBounded s)
    (ht : Bornology.IsBounded t) : Bornology.IsBounded (s * t) :=
  BoundedMul.isBounded_mul hs ht

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