mk_smul_set₀ — Mathlib

English

Let a be a nonzero element acting on a set s via a group action. The size of the image a·s equals the size of s.

Русский

Пусть a ≠ 0 действует на множество s; множество a·s и множество s имеют одинаковую кардинальность.

LaTeX

$$$\#(a \cdot s) = \#s$$$

Lean4

theorem _root_.Cardinal.mk_smul_set₀ (ha : a ≠ 0) (s : Set M₀) : #↥(a • s) = #s :=
  Cardinal.mk_image_eq_of_injOn _ _ (MulAction.injective₀ ha).injOn

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