lt_wf

Mathlib.Data.Finset.Card

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

← MathLib Explorer

English

The strict order on Finset α is well-founded.

Русский

Строгий порядок на Finset α является хорошо fundamento.

LaTeX

$$WellFounded (LT.lt) on Finset α$$

Lean4

theorem lt_wf {α} : WellFounded (@LT.lt (Finset α) _) :=
  have H : Subrelation (@LT.lt (Finset α) _) (InvImage (· < ·) card) := fun {_ _} hxy => card_lt_card hxy
  Subrelation.wf H <| InvImage.wf _ <| (Nat.lt_wfRel).2

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

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

Разделы

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

Аффилиация

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