wellFounded_iff — Mathlib

English

Well-foundedness is preserved under a surjective map that preserves the order up to an equivalence.

Русский

Связь хорошо сформированности сохраняется под сюръективным отображением, сохраняющим порядок через эквивалентность.

LaTeX

$$$\operatorname{WellFounded}\ r \iff \operatorname{WellFounded}\ s$ under surjective $f$ and order equivalence $r a b \iff s (f a)(f b)$$$

Lean4

theorem wellFounded_iff {f : α → β} (hf : Surjective f) (o : ∀ {a b}, r a b ↔ s (f a) (f b)) :
    WellFounded r ↔ WellFounded s :=
  Iff.intro (RelHomClass.wellFounded (⟨surjInv hf, fun h => by simpa only [o, surjInv_eq hf] using h⟩ : s →r r))
    (RelHomClass.wellFounded (⟨f, o.1⟩ : r →r s))

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