relIso_enum — Mathlib

English

For a RelIso f between r and s, the enum images coincide at the same index o up to a standard relabelling.

Русский

Для RelIso f между r и s образы enum совпадают на том же индексе o с учётом передачи relabelling.

LaTeX

$$$f( enum_r ⟨o, hr⟩ ) = enum_s ⟨o, hr.trans_eq (Quotient.sound ⟨f⟩)⟩$$$

Lean4

theorem relIso_enum {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
    (f : r ≃r s) (o : Ordinal) (hr : o < type r) : f (enum r ⟨o, hr⟩) = enum s ⟨o, hr.trans_eq (Quotient.sound ⟨f⟩)⟩ :=
  relIso_enum' _ _ _ _

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