encode_of_none_mem

Mathlib.Data.Sym.Basic

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

← MathLib Explorer

English

If none is a member of s, encode s is Sum.inl (s.erase none h).

Русский

Если none принадлежит s, кодирование s равно Sum.inl (s.erase none h).

LaTeX

$$$\\encode\\, s = \\text{Sum.inl}(s.erase\\, none\\, h)$ при $h : none \\in s$$$

Lean4

@[simp]
theorem encode_of_none_mem [DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∈ s) :
    encode s = Sum.inl (s.erase none h) :=
  dif_pos h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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