orderEmbOfFin_boundaries — Mathlib

English

The canonical order-embedding between Fin(c.length+1) and c.boundaries is exactly c.boundary.

Русский

Каноническое упорядоченное вложение между Fin(c.length+1) и c.boundaries совпадает с c.boundary.

LaTeX

$$$c.boundaries.orderEmbOfFin\\; c.card_boundaries_eq_succ_length = c.boundary$$$

Lean4

/-- The canonical increasing bijection between `Fin (c.length + 1)` and `c.boundaries` is
exactly `c.boundary`. -/
theorem orderEmbOfFin_boundaries : c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length = c.boundary :=
  by
  refine (Finset.orderEmbOfFin_unique' _ ?_).symm
  exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)

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