toWellOrderExtension_strictMono — Mathlib

English

The equivalence class of the embedding from α to WellOrderExtension α is strictly monotone.

Русский

Класс эквивалентности вложения из α в WellOrderExtension α является строго монотонным.

LaTeX

$$$\text{StrictMono}((toWellOrderExtension) : α \to WellOrderExtension α)$$$

Lean4

theorem toWellOrderExtension_strictMono [Preorder α] [WellFoundedLT α] :
    StrictMono (toWellOrderExtension : α → WellOrderExtension α) := fun _ _ h =>
  Prod.Lex.left _ _ <| IsWellFounded.rank_lt_of_rel h

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