typein_surjOn — Mathlib

English

The map typein r is surjective from the whole universe onto the initial segment Iio(type r).

Русский

Функция typein r сюръективна от всей вселенной на начальный отрезок Iio(type r).

LaTeX

$$Set.SurjOn (\\mathrm{typein}(r)) Set.univ (\\mathrm{Iio}(\\mathrm{type}(r)))$$

Lean4

theorem typein_surjOn (r : α → α → Prop) [IsWellOrder α r] : Set.SurjOn (typein r) Set.univ (Set.Iio (type r)) :=
  (typein r).surjOn

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