partiallyWellOrderedOn_insert

Mathlib.Order.WellFoundedSet

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

← MathLib Explorer

English

If t is PWOn by r and s ⊆ t, then s is PWOn by r.

Русский

Если t PWOn по r и s ⊆ t, то s PWOn по r.

LaTeX

$$(ht : t.PartiallyWellOrderedOn r) (h : s ⊆ t) : s.PartiallyWellOrderedOn r$$

Lean4

@[simp]
theorem partiallyWellOrderedOn_insert : PartiallyWellOrderedOn (insert a s) r ↔ PartiallyWellOrderedOn s r := by
  simp only [← singleton_union, partiallyWellOrderedOn_union, partiallyWellOrderedOn_singleton, true_and]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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