Documentation

Mathlib.Combinatorics.Additive.CovBySMul

Relation of covering by cosets #

This file defines a predicate for a set to be covered by at most K cosets of another set.

This is a fundamental relation to study in additive combinatorics.

def CovBySMul (M : Type u_1) {X : Type u_3} [Monoid M] [MulAction M X] (K : ) (A B : Set X) :

Predicate for a set A to be covered by at most K cosets of another set B under the action by the monoid M.

Equations
Instances For
    def CovByVAdd (M : Type u_1) {X : Type u_3} [AddMonoid M] [AddAction M X] (K : ) (A B : Set X) :

    Predicate for a set A to be covered by at most K cosets of another set B under the action by the monoid M.

    Equations
    Instances For
      @[simp]
      theorem CovBySMul.rfl {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A : Set X} :
      CovBySMul M 1 A A
      @[simp]
      theorem CovByVAdd.rfl {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A : Set X} :
      CovByVAdd M 1 A A
      @[simp]
      theorem CovBySMul.of_subset {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A B : Set X} (hAB : A B) :
      CovBySMul M 1 A B
      @[simp]
      theorem CovByVAdd.of_subset {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A B : Set X} (hAB : A B) :
      CovByVAdd M 1 A B
      theorem CovBySMul.nonneg {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : } {A B : Set X} :
      CovBySMul M K A B0 K
      theorem CovByVAdd.nonneg {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : } {A B : Set X} :
      CovByVAdd M K A B0 K
      @[simp]
      theorem covBySMul_zero {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A B : Set X} :
      CovBySMul M 0 A B A =
      @[simp]
      theorem covByVAdd_zero {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A B : Set X} :
      CovByVAdd M 0 A B A =
      theorem CovBySMul.mono {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K L : } {A B : Set X} (hKL : K L) :
      CovBySMul M K A BCovBySMul M L A B
      theorem CovByVAdd.mono {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K L : } {A B : Set X} (hKL : K L) :
      CovByVAdd M K A BCovByVAdd M L A B
      theorem CovBySMul.trans {M : Type u_1} {N : Type u_2} {X : Type u_3} [Monoid M] [Monoid N] [MulAction M X] [MulAction N X] {K L : } {A B C : Set X} [MulAction M N] [IsScalarTower M N X] (hAB : CovBySMul M K A B) (hBC : CovBySMul N L B C) :
      CovBySMul N (K * L) A C
      theorem CovByVAdd.trans {M : Type u_1} {N : Type u_2} {X : Type u_3} [AddMonoid M] [AddMonoid N] [AddAction M X] [AddAction N X] {K L : } {A B C : Set X} [AddAction M N] [VAddAssocClass M N X] (hAB : CovByVAdd M K A B) (hBC : CovByVAdd N L B C) :
      CovByVAdd N (K * L) A C
      theorem CovBySMul.subset_left {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : } {A₁ A₂ B : Set X} (hA : A₁ A₂) (hAB : CovBySMul M K A₂ B) :
      CovBySMul M K A₁ B
      theorem CovByVAdd.subset_left {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : } {A₁ A₂ B : Set X} (hA : A₁ A₂) (hAB : CovByVAdd M K A₂ B) :
      CovByVAdd M K A₁ B
      theorem CovBySMul.subset_right {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : } {A B₁ B₂ : Set X} (hB : B₁ B₂) (hAB : CovBySMul M K A B₁) :
      CovBySMul M K A B₂
      theorem CovByVAdd.subset_right {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : } {A B₁ B₂ : Set X} (hB : B₁ B₂) (hAB : CovByVAdd M K A B₁) :
      CovByVAdd M K A B₂
      theorem CovBySMul.subset {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {K : } {A₁ A₂ B₁ B₂ : Set X} (hA : A₁ A₂) (hB : B₁ B₂) (hAB : CovBySMul M K A₂ B₁) :
      CovBySMul M K A₁ B₂
      theorem CovByVAdd.subset {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {K : } {A₁ A₂ B₁ B₂ : Set X} (hA : A₁ A₂) (hB : B₁ B₂) (hAB : CovByVAdd M K A₂ B₁) :
      CovByVAdd M K A₁ B₂