wellFoundedOn

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.wellFoundedOn

English

A subsingleton set is well-founded with respect to any strict order.

Русский

Субодиночное множество хорошо основано относительно любого строгого порядка.

LaTeX

$$$\\operatorname{Subsingleton}(s) \\Rightarrow s.WellFoundedOn(r)$$$

Lean4

protected theorem wellFoundedOn (hs : s.Subsingleton) : s.WellFoundedOn r :=
  hs.finite.wellFoundedOn

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

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

Разделы

Аффилиация

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