eval_surjective — Mathlib

English

The evaluation at x is a morphism in the types category from the stalk to N.

Русский

Оценка в точке x является морфизмом в категории типов из сталка в N.

LaTeX

$$evalHom (x) : (smoothSheaf IM I M N).presheaf.stalk x → N$$

Lean4

/-- The `eval` map is surjective at `x`. -/
theorem eval_surjective (x : M) : Function.Surjective (smoothSheaf.eval IM I N x) :=
  by
  apply TopCat.stalkToFiber_surjective
  intro n
  exact ⟨⊤, fun _ ↦ n, contMDiff_const, rfl⟩

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