mathlib3

b337b921 - feat(model_theory/satisfiability): A union of a directed family of satisfiable theories is satisfiable (#13750)

feat(model_theory/satisfiability): A union of a directed family of satisfiable theories is satisfiable (#13750) Proves `first_order.language.Theory.is_satisfiable_directed_union_iff` - the union of a directed family of theories is satisfiable if and only if all of the theories in the family are satisfiable.