Theorems · Theorem · logic and foundations

Turing.ListBlank.map_mk

∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : List Γ),
  Turing.ListBlank.map f (Turing.ListBlank.mk l) = Turing.ListBlank.mk (List.map f.f l)

Defined in

Mathlib.Computability.TuringMachine.Tape

Cited by

1 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

InhabitedInhabited