English
Let α be a type with a binary operation. For finite sets s and t of α, if a ∈ t and the right-multiplication by a is injective, then |s| ≤ |s · t|.
Русский
Пусть α — множество с бинарной операцией. Пусть s и t — конечные подмножества α. Если a ∈ t и отображение x ↦ x · a инъективно, то |s| ≤ |s · t|.
LaTeX
$$$a \\in t \\wedge (\\forall x y, x \\cdot a = y \\cdot a \\rightarrow x = y) \\Rightarrow |s| \\le |s \\cdot t|$$$
Lean4
/-- See `card_le_card_mul_right` for a more convenient but less general version for types with a
right-cancellative multiplication.
-/
@[to_additive /-- See `card_le_card_add_right` for a more convenient but less general version for types with a
right-cancellative addition. -/
]
theorem card_le_card_mul_right_of_injective (hat : a ∈ t) (ha : Function.Injective (· * a)) : #s ≤ #(s * t) :=
card_le_card_image₂_right _ hat ha
