Theorems · Theorem · logic and foundations

Turing.ListBlank.flatMap_mk

∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (l : List Γ) (f : Γ → List Γ')
  (hf : ∃ n, f default = List.replicate n default),
  (Turing.ListBlank.mk l).flatMap f hf = Turing.ListBlank.mk (List.flatMap f l)

Defined in

Mathlib.Computability.TuringMachine.Tape

Cited by

0 results in Mathlib

Foundations

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

Assumes

InhabitedInhabited