Theorems · Theorem · logic and foundations

FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize

∀ {α : Type u_1} {A : Set ℕ} [Finite α] {n : ℕ}
  (φ : (FirstOrder.Language.presburger.withConstants ↑A).BoundedFormula α n),
  IsSemilinearSet {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}

Defined in: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Cited by: 1 results in Mathlib
Foundations: Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites59

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

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
AddCommMonoidproof · cited by 12,281
Equivproof · cited by 8,337
Fintypeproof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
Set.ofPredstatement and proof · cited by 6,101
Set.imageproof · cited by 5,609
Equiv.symmproof · cited by 3,681
Finitestatement and proof · cited by 3,029
Compl.complproof · cited by 2,925
FirstOrder.Languageproof · cited by 1,084

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinearproof · cited by 1