English
The same cardinality relation as above, with emphasis on nonempty case and its reflection in a simplified form.
Русский
Та же связь кардиналитетов, акцентированная на непустом случае и упрощенной форме.
LaTeX
$$$#s \le # (s * s)$; special case when s nonempty yields equality conditions$$
Lean4
/-- The size of `s * s` is at least the size of `s`, version with left-cancellative multiplication.
See `card_le_card_mul_self'` for the version with right-cancellative multiplication.
-/
@[to_additive /-- The size of `s + s` is at least the size of `s`, version with left-cancellative addition.
See `card_le_card_add_self'` for the version with right-cancellative addition. -/
]
theorem card_le_card_mul_self {s : Finset α} : #s ≤ #(s * s) := by
cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_left, *]
