coe_invEmbedding — Mathlib

English

For any composition c of n and any j ∈ Fin n, the inverse embedding at j satisfies (c.invEmbedding j) = j − sizeUpTo(index j).

Русский

Для композиции c размера n и любого j∈Fin n выполняется (c.invEmbedding j) = j − sizeUpTo(index j).

LaTeX

$$$ (c.invEmbedding j : \\mathbb{N}) = j - c.sizeUpTo (c.index j) $$$

Lean4

@[simp]
theorem coe_invEmbedding (j : Fin n) : (c.invEmbedding j : ℕ) = j - c.sizeUpTo (c.index j) :=
  rfl

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