mulETransformLeft — Mathlib

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)

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