emb_invEmbedding

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

URI: https://scilib.ai/kg/mathlib#OrderedFinpartition.emb_invEmbedding

English

For every j, embedding of the index and inverse embedding recovers j: c.emb (c.index j) (c.invEmbedding j) = j.

Русский

Для каждого j отображение вклада и его обратного вклада восстанавливают j.

LaTeX

$$$\\forall j,\\; c.emb (c.index j) (c.invEmbedding j) = j$$$

Lean4

@[simp]
theorem emb_invEmbedding (j : Fin n) : c.emb (c.index j) (c.invEmbedding j) = j :=
  (c.exists_inverse j).choose_spec

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru