mathlib documentation

data.finsupp.antidiagonal

The finsupp counterpart of multiset.antidiagonal. #

The antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.

noncomputable def finsupp.antidiagonal' {α : Type u_1} (f : α →₀ ) :

The finsupp counterpart of multiset.antidiagonal: the antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s. The finitely supported function antidiagonal s is equal to the multiplicities of these pairs.

Equations
noncomputable def finsupp.antidiagonal {α : Type u_1} (f : α →₀ ) :

The antidiagonal of s : α →₀ ℕ is the finset of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.

Equations
@[simp]
theorem finsupp.mem_antidiagonal {α : Type u_1} {f : α →₀ } {p : →₀ ) × →₀ )} :
theorem finsupp.swap_mem_antidiagonal {α : Type u_1} {n : α →₀ } {f : →₀ ) × →₀ )} :
theorem finsupp.antidiagonal_filter_fst_eq {α : Type u_1} (f g : α →₀ ) [D : Π (p : →₀ ) × →₀ )), decidable (p.fst = g)] :
finset.filter (λ (p : →₀ ) × →₀ )), p.fst = g) f.antidiagonal = ite (g f) {(g, f - g)}
theorem finsupp.antidiagonal_filter_snd_eq {α : Type u_1} (f g : α →₀ ) [D : Π (p : →₀ ) × →₀ )), decidable (p.snd = g)] :
finset.filter (λ (p : →₀ ) × →₀ )), p.snd = g) f.antidiagonal = ite (g f) {(f - g, g)}
@[simp]
theorem finsupp.antidiagonal_zero {α : Type u_1} :
0.antidiagonal = {(0, 0)}
theorem finsupp.sum_antidiagonal_swap {α : Type u_1} {M : Type u_2} [add_comm_monoid M] (n : α →₀ ) (f : →₀ )→₀ ) → M) :
∑ (p : →₀ ) × →₀ )) in n.antidiagonal, f p.fst p.snd = ∑ (p : →₀ ) × →₀ )) in n.antidiagonal, f p.snd p.fst
theorem finsupp.prod_antidiagonal_swap {α : Type u_1} {M : Type u_2} [comm_monoid M] (n : α →₀ ) (f : →₀ )→₀ ) → M) :
∏ (p : →₀ ) × →₀ )) in n.antidiagonal, f p.fst p.snd = ∏ (p : →₀ ) × →₀ )) in n.antidiagonal, f p.snd p.fst
noncomputable def finsupp.Iic_finset {α : Type u_1} (n : α →₀ ) :

The set {m : α →₀ ℕ | m ≤ n} as a finset.

Equations
@[simp]
theorem finsupp.mem_Iic_finset {α : Type u_1} {m n : α →₀ } :
@[simp]
theorem finsupp.coe_Iic_finset {α : Type u_1} (n : α →₀ ) :
theorem finsupp.finite_le_nat {α : Type u_1} (n : α →₀ ) :
{m : α →₀ | m n}.finite

Let n : α →₀ ℕ be a finitely supported function. The set of m : α →₀ ℕ that are coordinatewise less than or equal to n, is a finite set.

theorem finsupp.finite_lt_nat {α : Type u_1} (n : α →₀ ) :
{m : α →₀ | m < n}.finite

Let n : α →₀ ℕ be a finitely supported function. The set of m : α →₀ ℕ that are coordinatewise less than or equal to n, but not equal to n everywhere, is a finite set.