card_le_card_div_self — Mathlib

English

For any finite group, the inequality |S| ≤ |S / S| holds; in particular, if S is empty, both sides are handled separately, otherwise the inequality holds.

Русский

Для любой группы конечного множества выполняется |S| ≤ |S / S|; если S пусто, то соответствующие стороны трактуются отдельно, иначе неравенство выполняется.

LaTeX

$$Given any finite set S, |S| ≤ |S / S|$$

Lean4

@[to_additive]
theorem card_le_card_div_self : #s ≤ #(s / s) := by cases s.eq_empty_or_nonempty <;> simp [card_le_card_div_left, *]

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