Theorems · Theorem · logic and foundations

IsSemilinearSet.preimage

∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [AddMonoid.FG M] {F : Type u_5}
  [inst_3 : FunLike F M N] [AddMonoidHomClass F M N] {s : Set N},
  IsSemilinearSet s → ∀ (f : F), IsSemilinearSet (⇑f ⁻¹' s)

The preimage of a semilinear set under a homomorphism in a finitely generated monoid is semilinear.

Defined in

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidAddCommMonoidAddMonoid.FGFunLikeAddMonoidHomClass