wellFoundedGT — Mathlib

English

If β has well-founded GT, then α has well-founded GT via embedding.

Русский

Если β имеет хорошо основанное GT, то через вложение α также имеет хорошо основанное GT.

LaTeX

$$$[WellFoundedGT \\beta] (f : \\alpha \\hookrightarrow_o \\beta) \\Rightarrow WellFoundedGT(\\alpha).$$$

Lean4

/-- A preorder which embeds into a preorder in which `(· > ·)` is well-founded
also has `(· > ·)` well-founded. -/
protected theorem wellFoundedGT [WellFoundedGT β] (f : α ↪o β) : WellFoundedGT α :=
  @OrderEmbedding.wellFoundedLT αᵒᵈ _ _ _ _ f.dual

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