piAntidiag_empty_zero — Mathlib

English

The piAntidiag of the empty set and zero equals the singleton set containing the constant zero function.

Русский

piAntidiag пустого множества и нуля равен единичному множеству, содержащее константную нулевую функцию.

LaTeX

$$$\text{piAntidiag}(\emptyset,0) = \{0\}$$$

Lean4

@[simp]
theorem piAntidiag_empty_zero : piAntidiag (∅ : Finset ι) (0 : μ) = {0} := by ext; simp [funext_iff]

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