wellFoundedOn_singleton

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.wellFoundedOn_singleton

English

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

Русский

Множество из одного элемента хорошо основано относительно любого строгого порядка.

LaTeX

$$$\\forall a, (\\{a\\} \\text{ on } r).WellFoundedOn(r)$$$

Lean4

@[simp]
theorem wellFoundedOn_singleton : WellFoundedOn ({ a } : Set α) r :=
  (finite_singleton a).wellFoundedOn

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

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

Разделы

Аффилиация

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