Theorems · Theorem · logic and foundations

Turing.ToPartrec.Code.exists_code.comp

∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : Fin n → List.Vector ℕ m →. ℕ},
  (∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v) →
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((List.Vector.mOfFn fun i => g i v) >>= f)

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound