instWellFoundedLTSubtypeSetFinite

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#instWellFoundedLTSubtypeSetFinite

English

There is a WellFounded LT on the subtype { s ⊆ α | s.Finite }.

Русский

Существует WellFounded LT над подтипом {s ⊆ α | s конечен}.

LaTeX

$$$\\operatorname{WellFoundedLT}\\left(\\{ s : \\mathrm{Set}(\\alpha) \\mid s\\text{ finite} \\}\\right).$$$

Lean4

instance : WellFoundedLT { s : Set α // s.Finite } :=
  OrderIso.finsetSetFinite.symm.toOrderEmbedding.wellFoundedLT

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

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

Разделы

Аффилиация

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