wellFoundedGT — Mathlib

English

If f: α → β is strictly increasing and β has WellFoundedGT, then α has WellFoundedGT.

Русский

Пусть f: α → β строго возрастающая, и β имеет WellFoundedGT; тогда α имеет WellFoundedGT.

LaTeX

$$$\\forall {\\alpha \\beta} [Preorder \\alpha] [Preorder \\beta] {f : \\alpha \\to \\beta} [WellFoundedGT \\beta],\\; StrictMono f \\to WellFoundedGT \\alpha$$$

Lean4

theorem wellFoundedGT [WellFoundedGT β] (hf : StrictMono f) : WellFoundedGT α :=
  StrictMono.wellFoundedLT (α := αᵒᵈ) (β := βᵒᵈ) (fun _ _ h ↦ hf h)

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