theorem Metric.IsCover.image {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s C : Set X} {t : Set Y} {K ε : NNReal} (hf : LipschitzOnWith K f s) (hst : Set.SurjOn f s t) (hCs : C ⊆ s) (hC : IsCover ε s C) : IsCover (K * ε) t (f '' C)

theorem Metric.IsCover.prod {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {s C : Set X} {t D : Set Y} {ε : NNReal} (hC : IsCover ε s C) (hD : IsCover ε t D) : IsCover ε (s ×ˢ t) (C ×ˢ D)

theorem Metric.IsCover.pi {ε : NNReal} {ι : Type u_3} [Fintype ι] {X : ι → Type u_4} {I : Set ι} [(i : ι) → PseudoEMetricSpace (X i)] {s C : (i : ι) → Set (X i)} (hC : ∀ i ∈ I, IsCover ε (s i) (C i)) : IsCover ε (I.pi s) (I.pi C)