typein_enum

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.typein_enum

← MathLib Explorer

English

For any o with o < type r, typein r (enum r ⟨o,h⟩) = o.

Русский

Пусть o < type r; тогда typein r (enum r ⟨o,h⟩) = o.

LaTeX

$$$typein_r(\\mathrm{enum}_r(⟨o,h\\rangle)) = o$$$

Lean4

@[simp]
theorem typein_enum (r : α → α → Prop) [IsWellOrder α r] {o} (h : o < type r) : typein r (enum r ⟨o, h⟩) = o :=
  (typein r).apply_subrelIso _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru