ext — Mathlib

English

Two elements of x.toTopObj are equal if and only if their underlying coordinate functions are equal.

Русский

Два элемента из x.toTopObj равны тогда и только тогда, когда равны их координатные функции.

LaTeX

$$$\\forall x\\in \\text{SimplexCategory},\\; \\forall f,g\\in x^{\\mathrm{top}}: (f|=g) \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext {x : SimplexCategory} (f g : x.toTopObj) : (f : ToType x → ℝ≥0) = g → f = g :=
  Subtype.ext

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