union

Mathlib.Order.WellFoundedSet

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

English

If s and t are WF, then their union is WF.

Русский

Если множества s и t хорошо основаны, то их объединение тоже хорошо основано.

LaTeX

$$hs : IsWF s → ht : IsWF t → IsWF (s ∪ t)$$

Lean4

protected nonrec theorem union (hs : IsWF s) (ht : IsWF t) : IsWF (s ∪ t) :=
  hs.union ht

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

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

Разделы

Аффилиация

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