mulETransformRight — Mathlib

English

The right 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 \\cup e^{-1} \\cdot S, T \\cap 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 mulETransformRight : Finset α × Finset α :=
  (x.1 ∪ op e • x.1, x.2 ∩ e⁻¹ • x.2)

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