encodeSubtype — Mathlib

English

Let P be a decidable predicate on α. Then for any ⟨a,h⟩ with h : P a, encodeSubtype ⟨a,h⟩ = encode a.

Русский

Пусть P — детерминированное свойство на α. Тогда для любого элемента ⟨a,h⟩ с доказательством h : P a кодирование encodeSubtype ⟨a,h⟩ равно encode a.

LaTeX

$$$ encodeSubtype(\langle a,h \rangle) = encode(a) $$$

Lean4

/-- Explicit encoding function for a decidable subtype of an encodable type -/
def encodeSubtype : { a : α // P a } → ℕ
  | ⟨v, _⟩ => encode v

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