range_eval — Mathlib

English

If each α i is nonempty, then the range of the evaluation map eval i: (∀ i, α i) → α i is univ.

Русский

Если для каждого i тип α i непуст, то образ отображения eval i равен вселенной.

LaTeX

$$$ \\mathrm{range}(\\mathrm{eval}\\,i) = \\mathrm{univ}. $$$

Lean4

@[simp]
theorem range_eval {α : ι → Sort _} [∀ i, Nonempty (α i)] (i : ι) : range (eval i : (∀ i, α i) → α i) = univ :=
  (surjective_eval i).range_eq

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