antidiagonal — Mathlib

English

The antidiagonal of a multiset s consists of all pairs (t1,t2) with t1 + t2 = s, counted with multiplicities.

Русский

Антидиагональ мультимножества s состоит из всех пар (t1,t2), таких что t1 + t2 = s, считая повторения.

LaTeX

$$$$ \operatorname{antidiagonal}(s) = \{(t_1,t_2) \mid t_1 + t_2 = s\} $$$$

Lean4

/-- The antidiagonal of a multiset `s` consists of all pairs `(t₁, t₂)`
    such that `t₁ + t₂ = s`. These pairs are counted with multiplicities. -/
def antidiagonal (s : Multiset α) : Multiset (Multiset α × Multiset α) :=
  Quot.liftOn s (fun l ↦ (revzip (powersetAux l) : Multiset (Multiset α × Multiset α))) fun _ _ h ↦
    Quot.sound (revzip_powersetAux_perm h)

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