apply_surjective — Mathlib

English

Evaluation at a is a surjective map from Finsupp α M to M; given any m ∈ M there exists f = single a m with f a = m.

Русский

Оценка в точке a на множестве Finsupp α M сюръективна: для любого m ∈ M найдётся f = single a m с f(a)=m.

LaTeX

$$$$\\forall a\\colon \\alpha,\\; \\operatorname{Surjective}(f \\mapsto f(a))\\quad\\text{since } f=\\text{single}(a,m) \\text{ yields } f(a)=m.$$$$

Lean4

theorem apply_surjective (a : α) : Surjective fun f : α →₀ M ↦ f a :=
  RightInverse.surjective fun _ ↦ single_eq_same

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