wellFounded_liftOn₂'_iff — Mathlib

English

Well-foundedness of the lift-on-two-prime relation is equivalent to well-foundedness of the base relation.

Русский

Хорошо основанность liftOn₂' эквивалентна хорошему основанию базового отношения.

LaTeX

$$$\text{WellFounded}\big( x\mapsto x.liftOn₂' y\, r\, H\big) \iff \text{WellFounded } r$$$

Lean4

@[simp]
theorem wellFounded_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} :
    (WellFounded fun x y : Quotient s => Quotient.liftOn₂' x y r H) ↔ WellFounded r :=
  wellFounded_lift₂_iff (H := H)

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