wellFoundedGT — Mathlib

English

If f: α → β is strictly antitone and β is well-founded with respect to LT, then α is well-founded with respect to GT.

Русский

Если f: α → β строго антимонотонна, и β обоснована по LT, то α обоснована по GT.

LaTeX

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

Lean4

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

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