invEmbedding_comp — Mathlib

English

For any i ∈ Fin c.length and j ∈ Fin (c.blocksFun i), applying the embedding and then its inverse yields the original j: (c.invEmbedding (c.embedding i j) : ℕ) = j.

Русский

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

LaTeX

$$$ (c.invEmbedding (c.embedding i j) : \\mathbb{N}) = j $$$

Lean4

theorem invEmbedding_comp (i : Fin c.length) (j : Fin (c.blocksFun i)) : (c.invEmbedding (c.embedding i j) : ℕ) = j :=
  by simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]

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