preimage_mul_right_one — Mathlib

English

If s is a finite nonempty subset of α, then for any Finset t, the inequality |t| ≤ |s * t| holds, since left-multiplication by any element is injective.

Русский

Если s конечное непустое множество в α, то для любого Finset t выполняется |t| ≤ |s · t|, так как умножение слева на фиксированное значение инъективно.

LaTeX

$$$s \neq \varnothing \Rightarrow |t| \le |s \cdot t|$$$

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_right_one : preimage 1 (· * b) (mul_left_injective _).injOn = {b⁻¹} := by
  classical rw [← image_mul_right', image_one, one_mul]

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