preimage — Mathlib

English

If α is well-ordered by r and f: β ≃ α, then β is well-ordered by the preimage relation f^{-1} ∘ r.

Русский

Если α упорядочено хорошо по r и есть биекция f: β ≃ α, то β обладает хорошо упорядочением по предобразному отношению f^{-1} ∘ r.

LaTeX

$$$$ [IsWellOrder\ α\ r]\Rightarrow IsWellOrder\ β\ (f^{-1}\circ r). $$$$

Lean4

instance preimage {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : IsWellOrder β (f ⁻¹'o r) :=
  @RelEmbedding.isWellOrder _ _ (f ⁻¹'o r) r (RelIso.preimage f r) _

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