English
For finite sets s and t, the product s × t is nontrivial if and only if s and t are nonempty and at least one is nontrivial.
Русский
Для конечных множеств S и T произведение S × T не тривиально тогда и только тогда, когда S и T непусты и при этом хотя бы одно из них нетривиально.
LaTeX
$$$(s \\times t) \\neq \\emptyset \\iff (s \\neq \\emptyset) \\land (t \\neq \\emptyset) \\land (|s| > 1 \\lor |t| > 1)$$$
Lean4
/-- The product of two Finsets is nontrivial iff both are nonempty
at least one of them is nontrivial. -/
theorem nontrivial_prod_iff : (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial) := by
simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]; apply Nat.one_lt_mul_iff
