Commit 2025-11-26 13:03 e2bf3a6c

View on Github →

feat(Computability/NFA): NFA acceptsFrom definitions and lemmas (#31038) This PR defines NFA.acceptsFrom, similar to DFA.acceptsFrom, and provides helper lemmas.

Estimated changes

Modified Mathlib/Computability/NFA.lean

added def NFA.acceptsFrom

added theorem NFA.acceptsFrom_iUnion

added theorem NFA.acceptsFrom_iUnion₂

added theorem NFA.acceptsFrom_union

added theorem NFA.accepts_eq_acceptsFrom_start

added theorem NFA.append_mem_acceptsFrom

added theorem NFA.append_preimage_acceptsFrom

added theorem NFA.cons_mem_acceptsFrom

added theorem NFA.cons_preimage_acceptsFrom

added theorem NFA.evalFrom_append

added theorem NFA.evalFrom_iUnion

added theorem NFA.evalFrom_iUnion₂

added theorem NFA.evalFrom_union

modified theorem NFA.eval_append_singleton

added theorem NFA.mem_acceptsFrom

added theorem NFA.nil_mem_acceptsFrom

added theorem NFA.stepSet_union