surjective_eval — Mathlib

English

Assume every fiber β(a) is nonempty. Then for any a, the evaluation map eval_a: (∀ a, β a) → β a is surjective.

Русский

Пусть для каждого a множество β(a) непусто. Тогда отображение оценки eval_a: (∀ a, β(a)) → β(a) является сюръективным.

LaTeX

$$$\\forall a,\\ \\operatorname{Nonempty}(\\beta(a))\\Rightarrow \\operatorname{Surjective}(\\mathrm{eval}\\_a)$$$

Lean4

theorem surjective_eval {α : Sort u} {β : α → Sort v} [h : ∀ a, Nonempty (β a)] (a : α) :
    Surjective (eval a : (∀ a, β a) → β a) := fun b ↦
  ⟨@update _ _ (Classical.decEq α) (fun a ↦ (h a).some) a b, @update_self _ _ (Classical.decEq α) _ _ _⟩

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