isWF_union

Mathlib.Order.WellFoundedSet

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

English

IsWF(s ∪ t) is equivalent to IsWF s and IsWF t.

Русский

IsWF(s ∪ t) эквивалентно IsWF s и IsWF t.

LaTeX

$$IsWF(s ∪ t) \\iff (IsWF s ∧ IsWF t)$$

Lean4

@[simp]
theorem isWF_union : IsWF (s ∪ t) ↔ IsWF s ∧ IsWF t :=
  wellFoundedOn_union

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

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

Разделы

Аффилиация

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