index_embedding — Mathlib

English

For any i ∈ Fin c.length and j ∈ Fin (c.blocksFun i), the index of the embedding equals i: c.index (c.embedding i j) = i.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem index_embedding (i : Fin c.length) (j : Fin (c.blocksFun i)) : c.index (c.embedding i j) = i :=
  by
  symm
  rw [← mem_range_embedding_iff']
  apply Set.mem_range_self

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