isBounded_sub — Mathlib

English

If s and t are bounded subsets of a normed ring R with a Bornology, then s − t is bounded.

Русский

Если s и t — ограниченные подмножества кольца R, то множество их разности s − t ограничено.

LaTeX

$$$\forall \{R\}, [\mathrm{Bornology}(R)], [\mathrm{Sub} R], [\mathrm{BoundedSub} R],\forall s t\subseteq R,\ IsBounded(s) \Rightarrow IsBounded(t) \Rightarrow IsBounded(s \setminus t)$$$

Lean4

theorem isBounded_sub [Bornology R] [Sub R] [BoundedSub R] {s t : Set R} (hs : Bornology.IsBounded s)
    (ht : Bornology.IsBounded t) : Bornology.IsBounded (s - t) :=
  BoundedSub.isBounded_sub hs ht

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