wellFoundedOn

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.PartiallyWellOrderedOn.wellFoundedOn

English

If s is PWOn under r, then the induced order on s is well-founded.

Русский

Если s PWOn по r, то индуцированное на s упорядочение является well-founded.

LaTeX

$$$s.PartiallyWellOrderedOn r \\Rightarrow s.WellFoundedOn (\\\\lambda a b: r a b \\\\land \\\\neg r b a)$$$

Lean4

theorem wellFoundedOn (h : s.PartiallyWellOrderedOn r) : s.WellFoundedOn fun a b => r a b ∧ ¬r b a :=
  h.wellFounded

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

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

Разделы

Аффилиация

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