typein_surj

Mathlib.SetTheory.Ordinal.Basic

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

English

If o is less than the order type of r, then o lies in the range of typein r.

Русский

Если o меньше чем порядок типа r, то o лежит в образе typein r.

LaTeX

$$$o < \\mathrm{type}(r) \\Rightarrow o \\in \\mathrm{range}(\\mathrm{typein}(r))$$$

Lean4

theorem typein_surj (r : α → α → Prop) [IsWellOrder α r] {o} (h : o < type r) : o ∈ Set.range (typein r) :=
  (typein r).mem_range_of_rel_top h

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

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

Разделы

Аффилиация

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