smul_finset_inter

Mathlib.Algebra.Group.Action.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.smul_finset_inter

English

The smul distributes over intersection: a • (s ∩ t) = (a • s) ∩ (a • t).

Русский

Перенос через умножение распространяется на пересечение: a • (s ∩ t) = (a • s) ∩ (a • t).

LaTeX

$$$a \\cdot (s \\cap t) = (a \\cdot s) \\cap (a \\cdot t)$$$

Lean4

@[to_additive]
theorem smul_finset_inter : a • (s ∩ t) = a • s ∩ a • t :=
  image_inter _ _ <| MulAction.injective a

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

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

Разделы

Аффилиация

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