isWellOrder — Mathlib

English

If β is well-ordered by <, then α is well-ordered by < via an embedding f: α ↪o β.

Русский

Если β упорядочено хорошо по <, то через вложение f: α ↪o β α также является хорошо упорядоченным по <.

LaTeX

$$$[IsWellOrder(\\beta, <)] (f : \\alpha \\hookrightarrow_o \\beta) \\Rightarrow IsWellOrder(\\alpha, <).$$$

Lean4

protected theorem isWellOrder [IsWellOrder β (· < ·)] (f : α ↪o β) : IsWellOrder α (· < ·) :=
  f.ltEmbedding.isWellOrder

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