English
The left Dyson e-transform of (S,T) is (S ∩ e•S, T ∪ e^{-1}•T).
Русский
Левое преобразование Дайсона превращает (S,T) в (S ∩ e•S, T ∪ e^{-1}•T).
LaTeX
$$(S,T) \\mapsto (S \\cap e \\cdot S,\\; T \\cup e^{-1} \\cdot T)$$
Lean4
/-- An **e-transform**. Turns `(s, t)` into `(s ∩ s • e, t ∪ e⁻¹ • t)`. This reduces the
product of the two sets. -/
@[to_additive (attr := simps) /-- An **e-transform**.
Turns `(s, t)` into `(s ∩ s +ᵥ e, t ∪ -e +ᵥ t)`. This reduces the sum of the two sets. -/
]
def mulETransformLeft : Finset α × Finset α :=
(x.1 ∩ op e • x.1, x.2 ∪ e⁻¹ • x.2)