pointIndexEmbedding — Mathlib

English

The map from Fin(n+1) into PointsWithCircumcenterIndex n given by i ↦ pointIndex i is an embedding.

Русский

Отображение i ↦ pointIndex i из Fin(n+1) в PointsWithCircumcenterIndex n является вложением.

LaTeX

$$$\text{pointIndexEmbedding}(n):\ Fin(n+1) \hookrightarrow (\text{PointsWithCircumcenterIndex } n)$$$

Lean4

/-- `pointIndex` as an embedding. -/
def pointIndexEmbedding (n : ℕ) : Fin (n + 1) ↪ PointsWithCircumcenterIndex n :=
  ⟨fun i => pointIndex i, fun _ _ h => by injection h⟩

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