initialSegToType — Mathlib

English

Given ordinals α ≤ β, the initial segment embedding α.toType → β.toType exists and is well-defined.

Русский

Пусть α ≤ β; существует вложение начального сегмента α.toType → β.toType, образующее начальный сегмент.

LaTeX

$$$\text{initialSegToType}\;:\;\alpha\le\beta \to (\alpha.toType \le_i \beta.toType)$$$

Lean4

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

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