smul_set_symmDiff

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

English

Action distributes over symmetric difference: a • (s Δ t) = (a • s) Δ (a • t).

Русский

Действие над симметрической разностью: a • (s Δ t) = (a • s) Δ (a • t).

LaTeX

$$$a\cdot (s\Delta t) = (a\cdot s)\Delta (a\cdot t).$$$

Lean4

@[to_additive]
theorem smul_set_symmDiff : a • s ∆ t = (a • s) ∆ (a • t) :=
  image_symmDiff (MulAction.injective a) _ _

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

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

Разделы

Аффилиация

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