card_le_card_mul_self' — Mathlib

English

Let α be a cancellative semigroup. Then |s^2| ≥ |s| for any nonempty finite s. In particular, #s ≤ #(s s).

Русский

Пусть α — полугруппа с отменяемостью. Для любого непустого конечного множества S выполняется |S^2| ≥ |S|.

LaTeX

$$$$ \#s \le \#(s \cdot s). $$$$

Lean4

/-- The size of `s * s` is at least the size of `s`, version with right-cancellative multiplication.
See `card_le_card_mul_self` for the version with left-cancellative multiplication.
-/
@[to_additive /-- The size of `s + s` is at least the size of `s`, version with right-cancellative addition.
    See `card_le_card_add_self` for the version with left-cancellative addition. -/
    ]
theorem card_le_card_mul_self' : #s ≤ #(s * s) := by cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_right, *]

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