isVonNBounded_union — Mathlib

English

The union of two sets is von Neumann bounded iff both sets are von Neumann bounded.

Русский

Объединение двух множеств является von Neumann ограниченным тогда и только тогда, когда оба множества ограничены по von Neumann.

LaTeX

$$$\text{IsVonNBounded}_{𝕜}(s \cup t) \iff \text{IsVonNBounded}_{𝕜}(s) \land \text{IsVonNBounded}_{𝕜}(t)$$$

Lean4

@[simp]
theorem isVonNBounded_union {s t : Set E} : IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t := by
  simp only [IsVonNBounded, absorbs_union, forall_and]

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