English
Equality between trStmts and a product-based construction.
Русский
Равенство между trStmts и конструкцией на основе произведения.
LaTeX
$$stmts_trStmts_eq(M,S) : Eq (Turing.TM1to0.trStmts M S) (Finset.instSProd.sprod (TM1.stmts M S) Finset.univ)$$
Lean4
theorem exists_enc_dec [Inhabited Γ] [Finite Γ] :
∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
enc default = List.Vector.replicate n false ∧ ∀ a, dec (enc a) = a :=
by
rcases Finite.exists_equiv_fin Γ with ⟨n, ⟨e⟩⟩
letI : DecidableEq Γ := e.decidableEq
let G : Fin n ↪ Fin n → Bool :=
⟨fun a b ↦ a = b, fun a b h ↦ Bool.of_decide_true <| (congr_fun h b).trans <| Bool.decide_true rfl⟩
let H := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin _ _).symm.toEmbedding
let enc := H.setValue default (List.Vector.replicate n false)
exact ⟨_, enc, Function.invFun enc, H.setValue_eq _ _, Function.leftInverse_invFun enc.2⟩
