wellFoundedLT — Mathlib

English

If β has WellFoundedLT and f is strictly monotone, then α has WellFoundedLT.

Русский

Пусть β обладает WellFoundedLT и f строго монотонна; тогда α обладает WellFoundedLT.

LaTeX

$$$[\text{WellFoundedLT }\beta] \bigl( \operatorname{StrictMono}(f) \bigr) \Rightarrow \operatorname{WellFoundedLT}(\alpha)$$$

Lean4

theorem wellFoundedLT [WellFoundedLT β] (hf : StrictMono f) : WellFoundedLT α :=
  Subrelation.isWellFounded (InvImage (· < ·) f) @hf

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