isVonNBounded_sub_of_nonempty — Mathlib

English

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

Русский

Если s и t непусты, то s − t ограничено по фон Нейману тогда и только тогда, когда s и t ограничены по фон Нейману.

LaTeX

$$$\\text{If } s,t\\neq\\emptyset,\\quad \\operatorname{IsVonNBounded}_{\\mathbb{k}}(s - t) \\iff (\\operatorname{IsVonNBounded}_{\\mathbb{k}}(s) \\land \\operatorname{IsVonNBounded}_{\\mathbb{k}}(t)).$$$

Lean4

theorem isVonNBounded_sub_of_nonempty (hs : s.Nonempty) (ht : t.Nonempty) :
    IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t := by
  simp [sub_eq_add_neg, isVonNBounded_add_of_nonempty, hs, ht]

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