relIso_enum' — Mathlib

English

For an isomorphism of well-orders f, the map respects enum on initial segments: f(enum_r ⟨o,h⟩) equals enum_s ⟨o,hs⟩ with hs appropriate.

Русский

При изоморфизме хорошо упорядоченных множеств f сохраняет enum на начальных отрезках: f(enum_r ⟨o,h⟩) = enum_s ⟨o,hs⟩.

LaTeX

$$$\\forall o, hs\\,: f( enum_r ⟨o,hr⟩ ) = enum_s ⟨o,hs⟩$$$

Lean4

theorem relIso_enum' {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
    (f : r ≃r s) (o : Ordinal) : ∀ (hr : o < type r) (hs : o < type s), f (enum r ⟨o, hr⟩) = enum s ⟨o, hs⟩ :=
  by
  refine inductionOn o ?_; rintro γ t wo ⟨g⟩ ⟨h⟩
  rw [enum_type g, enum_type (g.transRelIso f)]; rfl

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