of_wellFoundedLT

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.IsWF.of_wellFoundedLT

English

If α has a well-founded LT, then every subset s has IsWF.

Русский

Если на α задано хорошо основанное LT, то любое подмножество s имеет IsWF.

LaTeX

$$[h : WellFoundedLT α] (s : Set α) : s.IsWF$$

Lean4

theorem of_wellFoundedLT [h : WellFoundedLT α] (s : Set α) : s.IsWF :=
  (Set.isWF_univ_iff.2 h).mono s.subset_univ

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

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

Разделы

Аффилиация

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