mem_range_typein_iff — Mathlib

English

For any ordinal o and well-order r, an element o belongs to the range of typein r exactly when o is smaller than type r.

Русский

Для любого элемента-ординала o и хорошего порядка r выражение o принадлежит диапазону typein r точь-в-точь тогда, когда o меньше type r.

LaTeX

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

Lean4

theorem mem_range_typein_iff (r : α → α → Prop) [IsWellOrder α r] {o} : o ∈ Set.range (typein r) ↔ o < type r :=
  (typein r).mem_range_iff_rel

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