isBounded_prod_of_nonempty — Mathlib

English

If s × t is nonempty, then s × t is bounded if and only if s and t are both bounded.

Русский

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

LaTeX

$$$(s \\times t \\neq \\varnothing) \\Rightarrow \\bigl((s \\times t) \\text{ bounded} \\iff (s \\text{ bounded} \\land t \\text{ bounded})\\bigr)$$$

Lean4

theorem isBounded_prod_of_nonempty (hne : Set.Nonempty (s ×ˢ t)) : IsBounded (s ×ˢ t) ↔ IsBounded s ∧ IsBounded t :=
  ⟨fun h => ⟨h.fst_of_prod hne.snd, h.snd_of_prod hne.fst⟩, fun h => h.1.prod h.2⟩

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