piAntidiag_empty — Mathlib

English

For any n, the piAntidiag of the empty index set is {0} if n = 0, and empty otherwise.

Русский

Для любого n piAntidiag пустого множества индексов равна {0}, если n = 0, и пусто иначе.

LaTeX

$$$\\pi\\mathrm{Antidiag}(\\emptyset, n) = \\begin{cases} \\{0\\} & \\text{если } n=0 \\\\ \\emptyset & \\text{если } n\\neq 0 \\end{cases}$$$

Lean4

theorem piAntidiag_empty (n : μ) : piAntidiag (∅ : Finset ι) n = if n = 0 then {0} else ∅ := by
  split_ifs with hn <;> simp [*]

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