Theorems · Theorem · logic and foundations

IsSemilinearSet.image

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

The image of a semilinear set under a homomorphism is semilinear.

Defined in

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Cited by

9 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidFunLikeAddMonoidHomClass