wellFoundedLT — Mathlib

English

A preorder that embeds into a well-founded LT-order has well-founded LT itself.

Русский

Любой порядок, который встраивается в хорошо основанный LT-порядок, сам имеет хорошо основанное LT-порядок.

LaTeX

$$$[IsWellOrder \\beta (\\lt)] (f : \\alpha \\hookrightarrow_o \\beta) \\Rightarrow WellFoundedLT(\\alpha).$$$

Lean4

/-- A preorder which embeds into a well-founded preorder is itself well-founded. -/
protected theorem wellFoundedLT [WellFoundedLT β] (f : α ↪o β) : WellFoundedLT α where
  wf := f.wellFounded IsWellFounded.wf

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