of_add_right — Mathlib

English

For any set S, VN boundedness of S + S is equivalent to VN boundedness of S.

Русский

VN‑ограниченность S + S эквивалентна VN‑ограниченности S.

LaTeX

$$isVonNBounded_add_self : IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s$$

Lean4

theorem of_add_right (hst : IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) : IsVonNBounded 𝕜 t :=
  let ⟨x, hx⟩ := hs
  (isVonNBounded_vadd x).mp <| hst.subset <| image_subset_image2_right hx

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