of_sub_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_sub_left (hst : IsVonNBounded 𝕜 (s - t)) (ht : t.Nonempty) : IsVonNBounded 𝕜 s :=
  ((sub_eq_add_neg s t).subst hst).of_add_left ht.neg

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