isWF

Mathlib.Order.WellFoundedSet

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

English

For a preorder α, the underlying set of a finite Finset s is well-founded on α.

Русский

Для предorder α множество, соответствующее конечному Finset s, хорошо основано на α.

LaTeX

$$[Preorder α] (s: Finset α) : (↑s : Set α).IsWF$$

Lean4

@[simp]
protected theorem isWF [Preorder α] (s : Finset α) : Set.IsWF (↑s : Set α) :=
  s.finite_toSet.isWF

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

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

Разделы

Аффилиация

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