instFunLikeElemForall — Mathlib

English

The projection that sends an element of the standard simplex to its coordinate function X → S is injective; the element is determined by its coordinates.

Русский

Проекция, отправляющая элемент стандартного симплекса на его координатную функцию, инъективна; элемент определяется его координатами.

LaTeX

$$$\operatorname{Injective}(\operatorname{Subtype.val} : (\mathrm{stdSimplex}\; S\; X).\mathrm{Elem} \to X \to S)$$$

Lean4

instance : FunLike (stdSimplex S X) X S where
  coe s := s.val
  coe_injective' := by aesop

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