finsuppAntidiag_empty_of_ne_zero

Mathlib.Algebra.Order.Antidiag.Finsupp

URI: https://scilib.ai/kg/mathlib#Finset.finsuppAntidiag_empty_of_ne_zero

← MathLib Explorer

English

If n ≠ 0, finsuppAntidiag ∅ n = ∅.

Русский

Если n ≠ 0, то finsuppAntidiag ∅ n = ∅.

LaTeX

$$finsuppAntidiag (∅ : Finset ι) n = ∅ \text{ if } n \neq 0$$

Lean4

@[simp]
theorem finsuppAntidiag_empty_of_ne_zero (hn : n ≠ 0) : finsuppAntidiag (∅ : Finset ι) n = ∅ :=
  eq_empty_of_forall_notMem (by simp [hn.symm])

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru