mem_finsuppAntidiag' — Mathlib

English

A refinement of the previous mem_finsuppAntidiag' statement, relating Iff to funext and HF contributions in Lean metadata.

Русский

Уточнение предыдущего утверждения о членстве в finsuppAntidiag'; связь через функциональное равенство и вложения в метаданных.

LaTeX

$$f ∈ finsuppAntidiag s n ↔ f.sum (fun _ x ↦ x) = n ∧ f.support ⊆ s$$

Lean4

theorem mem_finsuppAntidiag' : f ∈ finsuppAntidiag s n ↔ f.sum (fun _ x ↦ x) = n ∧ f.support ⊆ s :=
  by
  simp only [mem_finsuppAntidiag, and_congr_left_iff]
  rintro hf
  rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]

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