encodable — Mathlib

English

If α is encodable, then Finset α is encodable.

Русский

Если α кодируемый, то Finset α кодируемый.

LaTeX

$$$ (Encodable\\alpha) \\Rightarrow Encodable(\\mathrm{Finset}(\\alpha)) $$$

Lean4

/-- If `α` is encodable, then so is `Finset α`. -/
instance encodable [Encodable α] : Encodable (Finset α) :=
  haveI := decidableEqOfEncodable α
  ofEquiv { s : Multiset α // s.Nodup }
    { toFun := fun ⟨a, b⟩ => ⟨a, b⟩
      invFun := fun ⟨a, b⟩ => ⟨a, b⟩ }

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