encode_of_none_notMem — Mathlib

English

If none is not a member of s, encode s is Sum.inr (s.attach.map ...).

Русский

Если none не принадлежит s, кодирование s равно Sum.inr (s.attach.map ...).

LaTeX

$$$\\encode\\, s = \\mathrm{Sum.inr}(s.attach.map(\\ldots))$ при $none \\notin s$$$

Lean4

@[simp]
theorem encode_of_none_notMem [DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∉ s) :
    encode s = Sum.inr (s.attach.map fun o => o.1.get <| Option.ne_none_iff_isSome.1 <| ne_of_mem_of_not_mem o.2 h) :=
  dif_neg h

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