finite_smul_set — Mathlib

English

For a group action of G on a set α, the left translate a•s is finite if and only if s is finite.

Русский

Для действия группы G на множестве α множество a•S конечно тогда и только тогда, когда S конечно.

LaTeX

$$$ (a \\cdot S).\\operatorname{Finite} \\iff S.\\operatorname{Finite} $$$

Lean4

@[to_additive (attr := simp)]
theorem finite_smul_set : (a • s).Finite ↔ s.Finite :=
  finite_image_iff (MulAction.injective _).injOn

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