ext — Mathlib

English

Two standard-simplex functions are equal if they agree pointwise on all coordinates; i.e., extensionality for stdSimplex objects.

Русский

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

LaTeX

$$DFunLike.ext _ _ h$$

Lean4

@[ext]
theorem ext {n d : ℕ} (x y : Δ[n] _⦋d⦌) (h : ∀ (i : Fin (d + 1)), x i = y i) : x = y :=
  DFunLike.ext _ _ h

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