Commit 2026-04-17 08:05 9470b68e

View on Github →

feat(ModelTheory/Definablity): add DefinableFun definition and lemmas (#32744) This PR adds two basic shapes of definable sets and DefinableFun definition with relevant lemmas. The main result is Set.Definable.preimage_map asserting that the preimage of a definable set under a definable map is definable.

Estimated changes

Modified Mathlib/ModelTheory/Definability.lean

added theorem FirstOrder.Language.Term.definableFun_realize

added theorem FirstOrder.Language.definableFun_const

added theorem FirstOrder.Language.definableFun_var

added theorem Set.Definable.diagonal

added theorem Set.Definable.exists_of_finite

added theorem Set.Definable.forall_of_finite

added theorem Set.Definable.preimage_map

added theorem Set.Definable.singleton

added theorem Set.Definable.singleton_of_mem

added theorem Set.DefinableFun.comp

added theorem Set.DefinableFun.fun_symbol

added theorem Set.DefinableFun.ite

added theorem Set.DefinableFun.mono

added theorem Set.DefinableFun.of_empty

added theorem Set.DefinableFun.proj

added theorem Set.DefinableFun.setOf_eq

added theorem Set.DefinableFun.setOf_eq_const

added def Set.DefinableFun

added def Set.DefinableMap

added theorem Set.definableFun_iff_empty_definableFun_with_params

added theorem Set.definable_iInter_of_finite

added theorem Set.definable_iUnion_of_finite

added theorem Set.empty_definableFun_iff