acc_liftOn₂'_iff — Mathlib

English

Accessibility is preserved under liftOn₂' from Setoid to Quotients: Acc (liftOn₂') (mk'' a) iff Acc r a.

Русский

Доступность сохраняется под liftOn₂' от множества до фактор-отношения: Acc(liftOn₂')(mk'' a) эквивалентно Acc r a.

LaTeX

$$$Acc\big(\lambda x\, y,\, x.liftOn₂' y\, r\, H\big)(\mathrm{mk''}\, a) \iff Acc\, r\, a$$$

Lean4

@[simp]
theorem acc_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} {a} :
    Acc (fun x y => Quotient.liftOn₂' x y r H) (Quotient.mk'' a : Quotient s) ↔ Acc r a :=
  acc_lift₂_iff (H := H)

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