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.

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

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
      source
      def CovByVAdd (M : Type u_1) {X : Type u_3} [AddMonoid M] [AddAction M X] (K : ℝ) (A B : Set X) :
      Prop

      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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          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 B → 0 ≤ K
          source
          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 B → 0 ≤ K
          source
          @[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 = ∅
          source
          @[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 = ∅
          source
          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 B → CovBySMul M L A B
          source
          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 B → CovByVAdd M L A B
          source
          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} [SMul M N] [IsScalarTower M N X] (hAB : CovBySMul M K A B) (hBC : CovBySMul N L B C) :
          CovBySMul N (K * L) A C
          source
          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} [VAdd M N] [VAddAssocClass M N X] (hAB : CovByVAdd M K A B) (hBC : CovByVAdd N L B C) :
          CovByVAdd N (K * L) A C
          source
          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
          source
          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
          source
          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₂
          source
          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₂
          source
          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₂
          source
          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₂