instDenumerable — Mathlib

English

Code is denumerable: there exists a bijection between ℕ and Code (i.e., Code can be listed in a sequence).

Русский

Code перечислим: существует биекция между ℕ и Code (Code можно перечислить по порядку).

LaTeX

$$$\\mathrm{Denumerable}(\\mathrm{Code})$$$

Lean4

instance instDenumerable : Denumerable Code :=
  mk'
    ⟨encodeCode, ofNatCode, fun c => by induction c <;> simp [encodeCode, ofNatCode, Nat.div2_val, *], encode_ofNatCode⟩

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