isWellOrder

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelEmbedding.isWellOrder

English

If f : r ↪r s and s is a well-order, then r is a well-order.

Русский

Если f : r ↪r s и s хорошо упорядочено, то r хорошо упорядочено.

LaTeX

$$$\forall f:(r\hookrightarrow s), [\text{IsWellOrder } s] \Rightarrow \text{IsWellOrder } r$$$

Lean4

protected theorem isWellOrder : ∀ (_ : r ↪r s) [IsWellOrder β s], IsWellOrder α r
  | f, H => { f.isStrictTotalOrder with wf := f.wellFounded H.wf }

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

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

Разделы

Аффилиация

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