isBounded_prod — Mathlib

English

The product s × t is bounded precisely when either s or t is empty, or both s and t are bounded.

Русский

Произведение s × t ограничено тогда и только тогда, когда либо одно из множеств пусто, либо оба множества ограничены.

LaTeX

$$$(s \\times t)\\text{ bounded} \\iff (s = \\varnothing) \\lor (t = \\varnothing) \\lor ((s \\text{ bounded}) \\land (t \\text{ bounded}))$$$

Lean4

theorem isBounded_prod : IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t :=
  by
  rcases s.eq_empty_or_nonempty with (rfl | hs); · simp
  rcases t.eq_empty_or_nonempty with (rfl | ht); · simp
  simp only [hs.ne_empty, ht.ne_empty, isBounded_prod_of_nonempty (hs.prod ht), false_or]

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