ext — Mathlib

English

Two elements of stdSimplex S X are equal if their coordinate functions are equal; the representation is unique.

Русский

Два элемента stdSimplex S X равны, если равны их координатные функции; представление уникально.

LaTeX

$$$\forall s,t : (\mathrm{stdSimplex}\; S\; X).\mathrm{Elem},\ (s : X \to S) = (t : X \to S) \Rightarrow s = t$$$

Lean4

@[ext high]
theorem ext {s t : stdSimplex S X} (h : (s : X → S) = t) : s = t :=
  by
  ext : 1
  assumption

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