encard_smul_set

Mathlib.Algebra.Group.Pointwise.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_smul_set

English

For a group G acting on α and a ∈ G, the encard of a • s equals encard(s).

Русский

Для группы G, действующей на α, encard(a • s) = encard(s).

LaTeX

$$$$ (a \\cdot s).encard = s.encard $$$$

Lean4

@[to_additive (attr := simp)]
theorem encard_smul_set (a : G) (s : Set α) : (a • s).encard = s.encard := by simp [← toENat_cardinalMk]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru