boundary — Mathlib

English

There is a canonical increasing injection from the finite index set of boundaries to {0,1,...,n}.

Русский

Существует каноническое возрастающее вложение из множества границ в {0,1,...,n}.

LaTeX

$$boundary : Fin(c.boundaries.card) \hookrightarrow Fin(n+1)$$

Lean4

/-- Canonical increasing bijection from `Fin c.boundaries.card` to `c.boundaries`. -/
def boundary : Fin c.boundaries.card ↪o Fin (n + 1) :=
  c.boundaries.orderEmbOfFin rfl

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