ordinal_lift_type_eq — Mathlib

English

A RelIso between well-orders induces equality of lifted types.

Русский

Относительно-изоморфное отображение между хорошо упорядоченными множества между ординалами порождает равенство поднимаемых типов.

LaTeX

$$$\\operatorname{lift}(\\mathrm{type}(r)) = \\operatorname{lift}(\\mathrm{type}(s))$ for any RelIso f: r ≃r s.$$

Lean4

theorem _root_.RelIso.ordinal_lift_type_eq {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
    (f : r ≃r s) : lift.{v} (type r) = lift.{u} (type s) :=
  ((RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm).ordinal_type_eq

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