Theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective

Modification history

2024-08-26 23:29
Mathlib/ModelTheory/Complexity.lean
feat(ModelTheory/Complexity): Preservation theorems for atomic and quantifier-free formulas (#16108) …
Added FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injectiveView on Github →