typein_apply — Mathlib

English

If f is an order-embedding from r to s between well-orders, then applying typein in s to f(a) equals typein in r to a.

Русский

Если f — вложение по порядку между хорошо упорядоченными множествами r и s, то typein в s на f(a) даёт такое же число, как typein в r на a.

LaTeX

$$$\\text{typein}(s, f(a)) = \\text{typein}(r, a).$$$

Lean4

theorem typein_apply {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s)
    (a : α) : typein s (f a) = typein r a := by rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]

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