Closure of P under FP preimages

Main result

• mem_P_preimage — polynomial-time preprocessing preserves membership in P

theorem Complexity.mem_P_preimage {f : List Bool → List Bool} {L : Language} (hf : f ∈ FP) (hL : L ∈ P) : f ⁻¹' L ∈ P

If f is polynomial-time computable and L is polynomial-time decidable, then the preimage language {x | f x ∈ L} is in P.