decode_inr

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#SymOptionSuccEquiv.decode_inr

English

For every s in Sym α n.succ, decoding the right injection yields s mapped by some into the option type.

Русский

Для любого s ∈ Sym α n+1 разбор правого вложения даёт s, отображённое через some в типе Option α.

LaTeX

$$$\decode(\text{Sum.inr}(s)) = s.map(\mathrm{Embedding}.{\mathrm{some}})$$$

Lean4

@[simp]
theorem decode_inr (s : Sym α n.succ) : decode (Sum.inr s) = s.map Embedding.some :=
  rfl

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

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

Разделы

Аффилиация

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