isVonNBounded_add — Mathlib

English

IsVonNBounded(s+t) is equivalent to s=∅ or t=∅ or both IsVonNBounded(s) and IsVonNBounded(t).

Русский

IsVonNBounded(s+t) эквивалентно: s=∅ или t=∅ или оба множества ограничены Von Neumann.

LaTeX

$$$\text{IsVonNBounded}_{𝕜}(s+t) \iff s=\varnothing \lor t=\varnothing \lor \big(\text{IsVonNBounded}_{𝕜}(s) \land \text{IsVonNBounded}_{𝕜}(t)\big)$$$

Lean4

theorem isVonNBounded_add : IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t :=
  by
  rcases s.eq_empty_or_nonempty with rfl | hs; · simp
  rcases t.eq_empty_or_nonempty with rfl | ht; · simp
  simp [hs.ne_empty, ht.ne_empty, isVonNBounded_add_of_nonempty hs ht]

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