Finiteness lemmas for pointwise operations on sets

@[simp]

theorem Set.finite_smul_set {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : G} {s : Set α} : (a • s).Finite ↔ s.Finite

@[simp]

theorem Set.finite_vadd_set {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : G} {s : Set α} : (a +ᵥ s).Finite ↔ s.Finite

@[simp]

theorem Set.infinite_smul_set {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : G} {s : Set α} : (a • s).Infinite ↔ s.Infinite

@[simp]

theorem Set.infinite_vadd_set {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : G} {s : Set α} : (a +ᵥ s).Infinite ↔ s.Infinite

theorem Set.Finite.of_smul_set {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : G} {s : Set α} : (a • s).Finite → s.Finite

Alias of the forward direction of Set.finite_smul_set.

theorem Set.Finite.of_vadd_set {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : G} {s : Set α} : (a +ᵥ s).Finite → s.Finite

theorem Set.Infinite.smul_set {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : G} {s : Set α} : s.Infinite → (a • s).Infinite

Alias of the reverse direction of Set.infinite_smul_set.

theorem Set.Infinite.vadd_set {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : G} {s : Set α} : s.Infinite → (a +ᵥ s).Infinite