lift_typein_top — Mathlib

English

If f is a strict initial-segment embedding between r and s, then lifting the top element type satisfies a fixed equality.

Русский

Если f — строгое вложение начального сегмента между r и s, то подъем верхнего элемента типа удовлетворяет фиксированному равенству.

LaTeX

$$$\\text{lift}(\\mathrm{typein}(s, f.top)) = \\mathrm{lift}(\\mathrm{type}(r)).$$$

Lean4

@[simp]
theorem lift_typein_top {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≺i s) :
    lift.{u} (typein s f.top) = lift (type r) :=
  f.subrelIso.ordinal_lift_type_eq

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