English
Accessibility is preserved under quotient lift₂: Acc (Quotient.lift₂ r H) on the quotient equals Acc r on the representative.
Русский
Доступность (Acc) сохраняется под трамплином поэкзитивности (lift₂) на факторе: Acc(Quotient.lift₂ r H) на эквивалентном классе эквивалентно Acc r на представитель.
LaTeX
$$$Acc\big(\mathrm{Quotient.lift₂}\, r\, H\big)\big(\mathrm{Quotient.mk}\, a\big) \iff Acc\, r\, a$$$
Lean4
@[simp]
theorem acc_lift₂_iff {_ : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂}
{a} : Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a := by
constructor
· exact RelHomClass.acc (Quotient.mkRelHom H) a
· intro ac
induction ac with
| intro _ _ IH => ?_
refine ⟨_, fun q h => ?_⟩
obtain ⟨a', rfl⟩ := q.exists_rep
exact IH a' h
