principalSegToType — Mathlib

English

For ordinals α < β, the principal-seg embedding α.toType → β.toType exists and is well-defined.

Русский

Для ординалов α < β существует и определено вложение главной секции α.toType → β.toType.

LaTeX

$$$\text{principalSegToType}\;:\;\alpha<\beta \to (\alpha.toType

Lean4

/-- Given two ordinals `α < β`, then `principalSegToType α β` is the principal segment embedding of `α.toType` into `β.toType`. -/ def principalSegToType {α β : Ordinal} (h : α < β) : α.toType <i β.toType := by apply Classical.choice (type_lt_iff.mp _) rwa [type_toType, type_toType]

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