decidableRangeEncode — Mathlib

English

There is a decidable predicate for membership in the range of the encoding function.

Русский

Существует решаемый предикат принадлежности к диапазону кодирования.

LaTeX

$$$ \text{DecidablePred}(x \in \mathrm{Set.range}(\mathrm{encode}))$$$

Lean4

/-- The encoding function has decidable range. -/
def decidableRangeEncode (α : Type*) [Encodable α] : DecidablePred (· ∈ Set.range (@encode α _)) := fun x =>
  decidable_of_iff (Option.isSome (decode₂ α x))
    ⟨fun h => ⟨Option.get _ h, by rw [← decode₂_is_partial_inv (Option.get _ h), Option.some_get]⟩, fun ⟨n, hn⟩ => by
      rw [← hn, encodek₂]; exact rfl⟩

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