# Commit 2022-09-19 20:38 b3951c65

View on Github →feat(model_theory/*): Lemmas about satisfiability (#16546)
Proves that applying an injective language map to a theory does not change its satisfiability (`first_order.language.Theory.is_satisfiable_of_is_satisfiable_on_Theory`

)
Proves that a union of theories is satisfiable iff any finite union of the theories is (`first_order.language.Theory.is_satisfiable_Union_iff_is_satisfiable_Union_finset`

)
Proves a few other minor satisfiability and language map lemmas.