isBounded_union — Mathlib

English

The union of two bounded sets is bounded if and only if both are bounded.

Русский

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

LaTeX

$$$IsBounded (s \\cup t) \\iff IsBounded s \\land IsBounded t$$$

Lean4

@[simp]
theorem isBounded_union : IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t := by
  simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]

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