add — Mathlib

English

If s and t are von Neumann bounded, then their Minkowski sum s + t is also von Neumann bounded.

Русский

Если s и t VN‑ограничены, то их Minkowski сумма s + t ограничена по фон Нейману.

LaTeX

$$hs : IsVonNBounded 𝕜 s, ht : IsVonNBounded 𝕜 t ⇒ IsVonNBounded 𝕜 (s + t)$$

Lean4

protected theorem add (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) : IsVonNBounded 𝕜 (s + t) := fun U hU ↦
  by
  rcases exists_open_nhds_zero_add_subset hU with ⟨V, hVo, hV, hVU⟩
  exact ((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

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