def Finset.mulVCDim {G : Type u_1} [Group G] [DecidableEq G] (A B : Finset G) : ℕ

Equations

• A.mulVCDim B = (Finset.image (fun (x : G) => x • A ∩ B) (B / A)).vcDim

def Finset.addVCDim {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : ℕ

Equations

• A.addVCDim B = (Finset.image (fun (x : G) => (x +ᵥ A) ∩ B) (B - A)).vcDim

theorem Finset.mulVCDim_mono {G : Type u_1} [Group G] [DecidableEq G] {A B₁ B₂ : Finset G} (hB : B₁ ⊆ B₂) : A.mulVCDim B₁ ≤ A.mulVCDim B₂

theorem Finset.addVCDim_mono {G : Type u_1} [AddGroup G] [DecidableEq G] {A B₁ B₂ : Finset G} (hB : B₁ ⊆ B₂) : A.addVCDim B₁ ≤ A.addVCDim B₂