of_sub_right — Mathlib

English

If s − t is von Neumann bounded and s is nonempty, then t is von Neumann bounded.

Русский

Если множество s минус t ограничено по фон Нейману и множество s непусто, то множество t ограничено по фон Нейману.

LaTeX

$$$\\operatorname{IsVonNBounded}_{\\mathbb{k}}(s - t) \\quad \\land \\ s \\neq \\emptyset \\quad \\Rightarrow\\quad \\operatorname{IsVonNBounded}_{\\mathbb{k}}(t)$$$

Lean4

theorem of_sub_right (hst : IsVonNBounded 𝕜 (s - t)) (hs : s.Nonempty) : IsVonNBounded 𝕜 t :=
  (((sub_eq_add_neg s t).subst hst).of_add_right hs).of_neg

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