infinite_smul_set — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem infinite_smul_set : (a • s).Infinite ↔ s.Infinite :=
  infinite_image_iff (MulAction.injective _).injOn

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