TODO

Protected CovBySMul.rfl

theorem CovBySMul.pos {M : Type u_1} {X : Type u_3} [Monoid M] [MulAction M X] {A B : Set X} {K : ℝ} (hAB : CovBySMul M K A B) (hA : A.Nonempty) : 0 < K

theorem CovByVAdd.pos {M : Type u_1} {X : Type u_3} [AddMonoid M] [AddAction M X] {A B : Set X} {K : ℝ} (hAB : CovByVAdd M K A B) (hA : A.Nonempty) : 0 < K

theorem CovBySMul.prod {M : Type u_1} [Monoid M] {K L : ℝ} {N : Type u_4} [Group N] {A B : Set M} {C D : Set N} (hAB : CovBySMul M K A B) (hCD : CovBySMul N L C D) : CovBySMul (M × N) (K * L) (A ×ˢ C) (B ×ˢ D)

theorem CovByVAdd.sum {M : Type u_1} [AddMonoid M] {K L : ℝ} {N : Type u_4} [AddGroup N] {A B : Set M} {C D : Set N} (hAB : CovByVAdd M K A B) (hCD : CovByVAdd N L C D) : CovByVAdd (M × N) (K * L) (A ×ˢ C) (B ×ˢ D)

theorem CovBySMul.pi {ι : Type u_4} {G : ι → Type u_5} {X : ι → Type u_6} {s : Finset ι} [(i : ι) → Group (G i)] [(i : ι) → MulAction (G i) (X i)] {A B : (i : ι) → Set (X i)} {K : ι → ℝ} (hAB : ∀ i ∈ s, CovBySMul (G i) (K i) (A i) (B i)) : CovBySMul ((i : ι) → G i) (∏ i ∈ s, K i) ((↑s).pi A) ((↑s).pi B)

theorem CovByVAdd.pi {ι : Type u_4} {G : ι → Type u_5} {X : ι → Type u_6} {s : Finset ι} [(i : ι) → AddGroup (G i)] [(i : ι) → AddAction (G i) (X i)] {A B : (i : ι) → Set (X i)} {K : ι → ℝ} (hAB : ∀ i ∈ s, CovByVAdd (G i) (K i) (A i) (B i)) : CovByVAdd ((i : ι) → G i) (∏ i ∈ s, K i) ((↑s).pi A) ((↑s).pi B)

theorem CovBySMul.inter {G : Type u_2} [Group G] {A B C : Set G} {K L : ℝ} (hA : CovBySMul G K C A) (hB : CovBySMul G L C B) : CovBySMul G (K * L) C (A⁻¹ * A ∩ (B⁻¹ * B))

theorem CovByVAdd.inter {G : Type u_2} [AddGroup G] {A B C : Set G} {K L : ℝ} (hA : CovByVAdd G K C A) (hB : CovByVAdd G L C B) : CovByVAdd G (K * L) C ((-A + A) ∩ (-B + B))

theorem CovBySMul.iInter {G : Type u_2} [Group G] {B : Set G} {ι : Type u_4} {A : ι → Set G} {s : Finset ι} {K : ι → ℝ} (h : ∀ i ∈ s, CovBySMul G (K i) B (A i)) : CovBySMul G (∏ i ∈ s, K i) B (⋂ i ∈ s, (A i)⁻¹ * A i)

If B is covered by Kᵢ-many translates of each Aᵢ, then it is covered by ∏ᵢ Kᵢ-many translates of ⋂ᵢ Aᵢ⁻¹ * Aᵢ.

theorem covBySMul_mulOpposite_iff {G : Type u_2} [Group G] {A B : Set G} {K : ℝ} : CovBySMul Gᵐᵒᵖ K A B ↔ CovBySMul G K A⁻¹ B⁻¹

Covering B by K right translates of A is the same as covering B⁻¹ by K left translates of A⁻¹.

@[simp]

theorem univ_closedBall_one {G : Type u_2} [Group G] [PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] {K ε : ℝ} (hε : 0 ≤ ε) : CovBySMul G K Set.univ (Metric.closedBall 1 ε) ↔ ↑↑(Metric.coveringNumber ε.toNNReal Set.univ) ≤ ↑K