Theorems · Definition · logic and foundations
FirstOrder.Language.DefinableSet
(L : FirstOrder.Language) → {M : Type w} → [L.Structure M] → Set M → Type u₁ → Type (max 0 u₁ w)Definable sets are subsets of finite Cartesian products of a structure such that membership is given by a first-order formula.
- Defined in
- Mathlib.ModelTheory.Definability
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- Set.Definableproof · cited by 39
Cited by14
Results whose statement or proof uses this declaration.
- FirstOrder.Language.DefinableSet.le_iffstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.mem_complstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.mem_infstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.mem_sdiffstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.mem_supstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.mem_topstatement · cited by 0
- FirstOrder.Language.DefinableSet.notMem_botstatement · cited by 0
- FirstOrder.Language.DefinableSet.coe_botstatement · cited by 0
- FirstOrder.Language.DefinableSet.coe_complstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.coe_himpstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.coe_infstatement and proof · cited by 0
- FirstOrder.Language.DefinableSet.coe_sdiffstatement and proof · cited by 0