of_add_left — Mathlib

English

If s + t is VN bounded and s,t are nonempty, then both s and t are VN bounded.

Русский

Если s+t VN‑ограничено и s,t непустые, то оба множества VN‑ограничены.

LaTeX

$$hst : IsVonNBounded 𝕜 (s + t) → s.Nonempty → t.Nonempty → IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t$$

Lean4

theorem of_add_left (hst : IsVonNBounded 𝕜 (s + t)) (ht : t.Nonempty) : IsVonNBounded 𝕜 s :=
  ((add_comm s t).subst hst).of_add_right ht

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