Mathlib Map

Theorems · Definition · logic and foundations

IsSemilinearSet

{M : Type u_1} → [AddCommMonoid M] → Set M → Prop

A set is semilinear if it is a finite union of linear sets.

Defined in
Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Cited by
44 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Quot.sound
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsLinearSet.isSemilinearSet · cited by 10IsLinearSet.isSemilinearS…IsSemilinearSet.image · cited by 9IsSemilinearSet.imageIsSemilinearSet.biUnion · cited by 5IsSemilinearSet.biUnionIsSemilinearSet.union · cited by 3IsSemilinearSet.unionisSemilinearSet_image_iff · cited by 2isSemilinearSet_image_iffNat.isSemilinearSet_setOfPred_mulVec_eq · cited by 2Nat.isSemilinearSet_setOf…IsSemilinearSet.add · cited by 2IsSemilinearSet.addIsSemilinearSet.exists_fg_eq_subtypeVal₂ · cited by 2IsSemilinearSet.exists_fg…IsSemilinearSet.inter · cited by 2IsSemilinearSet.interIsSemilinearSet.proj · cited by 2IsSemilinearSet.projIsSemilinearSet.sInter · cited by 2IsSemilinearSet.sInterIsSemilinearSet.sUnion · cited by 2IsSemilinearSet.sUnionisSemilinearSet_iff · cited by 1isSemilinearSet_iffisSemilinearSet_setOfPred_eq · cited by 1isSemilinearSet_setOfPred…FirstOrder.Language.presburger.definable_iff_isSemilinearSet · cited by 1presburger.definable_iff_…Set · cited by 53352SetAddCommMonoid · cited by 12281AddCommMonoidSet.Finite · cited by 1814Set.FiniteSet.sUnion · cited by 392Set.sUnionIsLinearSet · cited by 28IsLinearSetIsSemilinearSetCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by44

Results whose statement or proof uses this declaration.