Definability

📁 Source: Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean

Statistics

Metric	Count
Definitions	0
Theorems definable_iff_isSemilinearSet, definable₁_iff_ultimately_periodic, isSemilinearSet_boundedFormula_realize, isSemilinearSet_formula_realize_semilinear, mul_not_definable, term_realize_eq_add_dotProduct, definable, definable	8
Total	8

FirstOrder.Language.presburger

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
definable_iff_isSemilinearSet 📖	mathematical	—	Set.Definable FirstOrder.Language.presburger instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne IsSemilinearSet Pi.addCommMonoid Nat.instAddCommMonoid	—	isSemilinearSet_formula_realize_semilinear IsSemilinearSet.definable
definable₁_iff_ultimately_periodic 📖	mathematical	—	Set.Definable₁ FirstOrder.Language.presburger instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne Set Set.instMembership	—	Set.Definable₁.eq_1 definable_iff_isSemilinearSet Finite.of_fintype RingHomInvPair.ids isSemilinearSet_image_iff SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass Set.preimage_setOf_eq Set.image_congr Set.image_preimage_eq Nat.isSemilinearSet_iff_ultimately_periodic
isSemilinearSet_boundedFormula_realize 📖	mathematical	—	IsSemilinearSet Pi.addCommMonoid Nat.instAddCommMonoid setOf FirstOrder.Language.BoundedFormula.Realize FirstOrder.Language.withConstants FirstOrder.Language.presburger Set.Elem FirstOrder.Language.withConstantsStructure instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne FirstOrder.Language.paramsStructure	—	IsSemilinearSet.empty term_realize_eq_add_dotProduct Matrix.cons_mulVec Matrix.empty_mulVec Matrix.add_cons Matrix.tail_cons Matrix.empty_add_empty Nat.isSemilinearSet_setOf_mulVec_eq Set.setOf_inter_eq_sep IsSemilinearSet.compl Pi.instAddMonoidFG Finite.of_fintype AddMonoid.instFGNat IsSemilinearSet.inter RingHomInvPair.ids Fin.snoc_last finSumFinEquiv_symm_last Fin.cons_zero Fin.snoc_castSucc finSumFinEquiv_symm_apply_castSucc IsSemilinearSet.proj isSemilinearSet_image_iff SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass
isSemilinearSet_formula_realize_semilinear 📖	mathematical	—	IsSemilinearSet Pi.addCommMonoid Nat.instAddCommMonoid setOf FirstOrder.Language.Formula.Realize FirstOrder.Language.withConstants FirstOrder.Language.presburger Set.Elem FirstOrder.Language.withConstantsStructure instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne FirstOrder.Language.paramsStructure	—	Fin.isEmpty' Set.ext Equiv.exists_congr_left Unique.eq_default IsSemilinearSet.image DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass isSemilinearSet_boundedFormula_realize
mul_not_definable 📖	mathematical	—	Set.Definable FirstOrder.Language.presburger instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne setOf	—	Set.Definable₁.eq_1 Set.ext Set.image_congr Matrix.cons_val_fin_one Fin.cons_zero Fin.cons_one Set.Definable.image_comp Set.Definable.preimage_comp Finite.of_fintype definable₁_iff_ultimately_periodic LE.le.trans' le_max_left
term_realize_eq_add_dotProduct 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.withConstants FirstOrder.Language.presburger Set.Elem FirstOrder.Language.withConstantsStructure instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne FirstOrder.Language.paramsStructure dotProduct Nat.instAddCommMonoid	—	single_dotProduct one_mul zero_add FirstOrder.Language.withConstants_funMap_sumInl FirstOrder.Language.withConstants_expansion zero_dotProduct add_zero add_dotProduct add_left_comm add_assoc FirstOrder.Language.withConstants_funMap_sumInr

IsLinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
definable 📖	mathematical	IsLinearSet Pi.addCommMonoid Nat.instAddCommMonoid	Set.Definable FirstOrder.Language.presburger FirstOrder.Language.presburger.instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne	—	isLinearSet_iff Finite.of_fintype Set.ext Finset.sum_congr nsmul_eq_mul FirstOrder.Language.Term.realize_varsToConstants FirstOrder.Language.withConstants_expansion FirstOrder.Language.presburger.realize_natCast FirstOrder.Language.presburger.realize_sum FirstOrder.Language.presburger.realize_nsmul mul_comm Finset.sum_apply

IsSemilinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
definable 📖	mathematical	IsSemilinearSet Pi.addCommMonoid Nat.instAddCommMonoid	Set.Definable FirstOrder.Language.presburger FirstOrder.Language.presburger.instStructure MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne	—	isSemilinearSet_iff Finite.of_fintype Set.ext Set.ext_iff IsLinearSet.definable

---

← Back to Index