isBounded_prod_self — Mathlib

English

The product s × s is bounded if and only if s is bounded.

Русский

Произведение s × s ограничено тогда, когда и только когда s ограничено.

LaTeX

$$$(s \\times s) \\text{ bounded} \\iff s \\text{ bounded}$$$

Lean4

theorem isBounded_prod_self : IsBounded (s ×ˢ s) ↔ IsBounded s :=
  by
  rcases s.eq_empty_or_nonempty with (rfl | hs); · simp
  exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

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