Theorems · Theorem · logic and foundations

Turing.ListBlank.map_modifyNth

∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (F : Turing.PointedMap Γ Γ') (f : Γ → Γ)
  (f' : Γ' → Γ'),
  (∀ (x : Γ), F.f (f x) = f' (F.f x)) →
    ∀ (n : ℕ) (L : Turing.ListBlank Γ),
      Turing.ListBlank.map F (Turing.ListBlank.modifyNth f n L) =
        Turing.ListBlank.modifyNth f' n (Turing.ListBlank.map F L)

Defined in

Mathlib.Computability.TuringMachine.Tape

Cited by

1 results in Mathlib

Foundations

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

Assumes

InhabitedInhabited