English
Well-foundedness is preserved under a RelEmbedding: if f : r ↪r s and s is well-founded, then r is well-founded.
Русский
Хорошо основано через вложение отношений: если f : r ↪r s и s хорошо основано, то r хорошо основано.
LaTeX
$$$\forall f:(r\hookrightarrow s),\text{WellFounded}(s)\Rightarrow \text{WellFounded}(r)$$$
Lean4
/-- A relation is well founded iff its lift to a quotient is. -/
@[simp]
theorem wellFounded_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
{H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} :
WellFounded (Quotient.lift₂ r H) ↔ WellFounded r :=
by
constructor
· exact RelHomClass.wellFounded (Quotient.mkRelHom H)
· refine fun wf => ⟨fun q => ?_⟩
obtain ⟨a, rfl⟩ := q.exists_rep
exact acc_lift₂_iff.2 (wf.apply a)
