embedding_comp_inv — Mathlib

English

For any i ∈ Fin c.length and j ∈ Fin (c.blocksFun i), the embedding of i and j maps back to the original index: c.embedding (c.index j) (c.invEmbedding j) = j.

Русский

Для любой пары i ∈ Fin c.length и j ∈ Fin (c.blocksFun i) вложение c.embedding i j возвращает исходный индекс: c.index (c.embedding i j) = i.

LaTeX

$$$ c.embedding (c.index j) (c.invEmbedding j) = j $$$

Lean4

@[simp]
theorem embedding_comp_inv (j : Fin n) : c.embedding (c.index j) (c.invEmbedding j) = j :=
  by
  rw [Fin.ext_iff]
  apply add_tsub_cancel_of_le (c.sizeUpTo_index_le j)

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