finsuppAntidiag — Mathlib

English

Characterization of finsuppAntidiag: f ∈ finsuppAntidiag s n iff s.sum f = n and f.support ⊆ s.

Русский

Характеризация finsuppAntidiag: f ∈ finsuppAntidiag s n тогда и только тогда, когда сумма по s равна n и опорf ⊆ s.

LaTeX

$$f ∈ finsuppAntidiag s n \Leftrightarrow s.sum f = n ∧ f.support ⊆ s$$

Lean4

/-- The finset of functions `ι →₀ μ` with support contained in `s` and sum equal to `n`. -/
def finsuppAntidiag (s : Finset ι) (n : μ) : Finset (ι →₀ μ) :=
  (piAntidiag s n).attach.map
    ⟨fun f ↦ ⟨s.filter (f.1 · ≠ 0), f.1, by simpa using (mem_piAntidiag.1 f.2).2⟩, fun _ _ hfg ↦
      Subtype.ext (congr_arg (⇑) hfg)⟩

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