Theorems · Theorem · logic and foundations

IsLinearSet.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}, IsLinearSet s → ∀ (f : F), IsLinearSet (⇑f '' s)

Defined in: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Cited by: 1 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid AddCommMonoid FunLike AddMonoidHomClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
AddCommMonoidstatement and proof · cited by 12,281
SetLike.coeproof · cited by 8,199
Set.imagestatement and proof · cited by 5,609
FunLikestatement and proof · cited by 2,560
HVAdd.hVAddproof · cited by 1,820
Set.Finiteproof · cited by 1,814
AddMonoidHomClassstatement and proof · cited by 252
AddSubmonoid.closureproof · cited by 224
Set.Finite.imageproof · cited by 96
IsLinearSetstatement and proof · cited by 28

Cited by1

Results whose statement or proof uses this declaration.

IsSemilinearSet.imageproof · cited by 9