wellFoundedLT — Mathlib

English

Let α and β be preordered types and f: α → β be strictly antitone. If β is well-founded with respect to the GT relation, then α is well-founded with respect to the LT relation.

Русский

Пусть α и β — множества с пред-, упорядочениями, f: α → β строго антимонотонна. Если β имеет обоснованность относительно отношения >, то α имеет обоснованность относительно <.

LaTeX

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

Lean4

theorem wellFoundedLT [WellFoundedGT β] (hf : StrictAnti f) : WellFoundedLT α :=
  StrictMono.wellFoundedLT (β := βᵒᵈ) hf

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