sub — Mathlib

English

Let I be finite and s_i ⊆ E. The VN boundedness of ⋃ i∈I s_i is equivalent to the VN boundedness of each s_i with i ∈ I.

Русский

Пусть I конечно; ⋃_{i∈I} s_i VN‑ограничено тогда и только тогда, когда каждый s_i VN‑ограничен для i∈I.

LaTeX

$$I.Finite → IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)$$

Lean4

protected theorem sub (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) : IsVonNBounded 𝕜 (s - t) :=
  by
  rw [sub_eq_add_neg]
  exact hs.add ht.neg

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