Set.Infinite.smul_set
theorem Set.Infinite.smul_set :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
s.Infinite → (a • s).Infinite
This theorem, referred to as an alias of the reverse direction of `Set.infinite_smul_set`, states that for any types `α` and `β`, given `α` is a group and there exists a multiplication action from `α` to `β`, for any element `a` of type `α` and any set `s` of type `β`, if `s` is infinite, then the set resulting from the scalar multiplication of `s` with `a` is also infinite. In other words, scaling an infinite set by any element from a group results in another infinite set.
More concisely: If `α` is a group and `α` acts multiplicatively on a set `β` such that `β` is infinite, then the scalar multiplication of `β` by any element `a` in `α` also results in an infinite set.
|
Set.Finite.of_smul_set
theorem Set.Finite.of_smul_set :
∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
(a • s).Finite → s.Finite
This theorem, referred to as an "Alias" of the forward direction of `Set.finite_smul_set`, states that for any types `α` and `β`, where `α` is a group and `β` is an `α`-mulAction, and for any element `a` of `α` and set `s` of `β`, if the set resulting from scalar multiplication of `s` by `a` (denoted by `a • s`) is finite, then the original set `s` is also finite. Essentially, if the scalar multiplication of a set by an element of a group yields a finite set, then the original set must have been finite as well.
More concisely: If `α` is a group, `β` an `α`-module, `a` an element of `α`, and `s` a finite subset of `β`, then `a • s` is also a finite subset of `β`.
|