mono

Mathlib.Order.WellFounded

URI: https://scilib.ai/kg/mathlib#WellFounded.mono

English

If r is well-founded and r' is contained in r via h, then r' is well-founded.

Русский

Если r хорошо основано и r' ограничено r через h, то r' хорошо основано.

LaTeX

$$$WellFounded\ r \to (\forall a b, r' a b \to r a b) \to WellFounded\ r'$$$

Lean4

theorem mono (hr : WellFounded r) (h : ∀ a b, r' a b → r a b) : WellFounded r' :=
  Subrelation.wf (h _ _) hr

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

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

Разделы

Аффилиация

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