decodeSubtype — Mathlib

English

Let α, P as above. For v ∈ ℕ, decodeSubtype v returns Some ⟨a,h⟩ whenever decode v = Some a and P a holds; otherwise it returns None.

Русский

Пусть α, P как выше. Для любого v ∈ ℕ декодирование decodeSubtype v возвращает Some ⟨a,h⟩ тогда и только тогда, когда decode v = Some a и P a истинно; иначе возвращает None.

LaTeX

$$$ decodeSubtype(v) = (decode(v)).bind(\lambda a. \text{if } h : P a \text{ then Some } \langle a,h \rangle \text{ else } None)$$$

Lean4

/-- Explicit decoding function for a decidable subtype of an encodable type -/
def decodeSubtype (v : ℕ) : Option { a : α // P a } :=
  (decode v).bind fun a => if h : P a then some ⟨a, h⟩ else none

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