isPWO_support_mulAntidiagonal

Mathlib.Data.Finset.MulAntidiagonal

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

← MathLib Explorer

English

The set {a | (mulAntidiagonal hs ht a).Nonempty} is well-founded (under the induced order).

Русский

Множество {a | (mulAntidiagonal hs ht a).Nonempty} является хорошо упорядоченным.

LaTeX

$$ {a | (mulAntidiagonal hs ht a).Nonempty}.IsPWO$$

Lean4

@[to_additive]
theorem isPWO_support_mulAntidiagonal : {a | (mulAntidiagonal hs ht a).Nonempty}.IsPWO :=
  (hs.mul ht).mono support_mulAntidiagonal_subset_mul

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

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

Разделы

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

Аффилиация

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