Finiteness lemmas for pointwise operations on sets #
theorem
Set.Finite.neg
{α : Type u_2}
[InvolutiveNeg α]
{s : Set α}
(hs : Set.Finite s)
:
Set.Finite (-s)
theorem
Set.Finite.add
{α : Type u_2}
[Add α]
{s : Set α}
{t : Set α}
:
Set.Finite s → Set.Finite t → Set.Finite (s + t)
theorem
Set.Finite.mul
{α : Type u_2}
[Mul α]
{s : Set α}
{t : Set α}
:
Set.Finite s → Set.Finite t → Set.Finite (s * t)
instance
Set.decidableMemAdd
{α : Type u_2}
[AddMonoid α]
{s : Set α}
{t : Set α}
[Fintype α]
[DecidableEq α]
[DecidablePred fun x => x ∈ s]
[DecidablePred fun x => x ∈ t]
:
DecidablePred fun x => x ∈ s + t
instance
Set.decidableMemMul
{α : Type u_2}
[Monoid α]
{s : Set α}
{t : Set α}
[Fintype α]
[DecidableEq α]
[DecidablePred fun x => x ∈ s]
[DecidablePred fun x => x ∈ t]
:
DecidablePred fun x => x ∈ s * t
theorem
Set.decidableMemNSMul.proof_1
{α : Type u_1}
[AddMonoid α]
{s : Set α}
:
(DecidablePred fun x => x ∈ Nat.zero • s) = DecidablePred fun x => x = 0
theorem
Set.decidableMemNSMul.proof_2
{α : Type u_1}
[AddMonoid α]
{s : Set α}
(n : ℕ)
:
(DecidablePred fun x => x ∈ Nat.succ n • s) = DecidablePred fun x => x ∈ s + n • s
instance
Set.decidableMemNSMul
{α : Type u_2}
[AddMonoid α]
{s : Set α}
[Fintype α]
[DecidableEq α]
[DecidablePred fun x => x ∈ s]
(n : ℕ)
:
DecidablePred fun x => x ∈ n • s
instance
Set.decidableMemPow
{α : Type u_2}
[Monoid α]
{s : Set α}
[Fintype α]
[DecidableEq α]
[DecidablePred fun x => x ∈ s]
(n : ℕ)
:
DecidablePred fun x => x ∈ s ^ n
theorem
Set.Finite.vadd
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Finite s → Set.Finite t → Set.Finite (s +ᵥ t)
theorem
Set.Finite.smul
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set α}
{t : Set β}
:
Set.Finite s → Set.Finite t → Set.Finite (s • t)
theorem
Set.Finite.vadd_set
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set β}
{a : α}
:
Set.Finite s → Set.Finite (a +ᵥ s)
theorem
Set.Finite.smul_set
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set β}
{a : α}
:
Set.Finite s → Set.Finite (a • s)
theorem
Set.Infinite.of_vadd_set
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set β}
{a : α}
:
Set.Infinite (a +ᵥ s) → Set.Infinite s
theorem
Set.Infinite.of_smul_set
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set β}
{a : α}
:
Set.Infinite (a • s) → Set.Infinite s
theorem
Set.Finite.vsub
{α : Type u_2}
{β : Type u_3}
[VSub α β]
{s : Set β}
{t : Set β}
(hs : Set.Finite s)
(ht : Set.Finite t)
:
Set.Finite (s -ᵥ t)
theorem
Set.infinite_add
{α : Type u_2}
[Add α]
[IsLeftCancelAdd α]
[IsRightCancelAdd α]
{s : Set α}
{t : Set α}
:
Set.Infinite (s + t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
theorem
Set.infinite_mul
{α : Type u_2}
[Mul α]
[IsLeftCancelMul α]
[IsRightCancelMul α]
{s : Set α}
{t : Set α}
:
Set.Infinite (s * t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
@[simp]
theorem
Set.finite_vadd_set
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddAction α β]
{a : α}
{s : Set β}
:
Set.Finite (a +ᵥ s) ↔ Set.Finite s
@[simp]
theorem
Set.finite_smul_set
{α : Type u_2}
{β : Type u_3}
[Group α]
[MulAction α β]
{a : α}
{s : Set β}
:
Set.Finite (a • s) ↔ Set.Finite s
@[simp]
theorem
Set.infinite_vadd_set
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddAction α β]
{a : α}
{s : Set β}
:
Set.Infinite (a +ᵥ s) ↔ Set.Infinite s
@[simp]
theorem
Set.infinite_smul_set
{α : Type u_2}
{β : Type u_3}
[Group α]
[MulAction α β]
{a : α}
{s : Set β}
:
Set.Infinite (a • s) ↔ Set.Infinite s
theorem
Set.Finite.of_smul_set
{α : Type u_2}
{β : Type u_3}
[Group α]
[MulAction α β]
{a : α}
{s : Set β}
:
Set.Finite (a • s) → Set.Finite s
Alias of the forward direction of Set.finite_smul_set
.
theorem
Set.Infinite.smul_set
{α : Type u_2}
{β : Type u_3}
[Group α]
[MulAction α β]
{a : α}
{s : Set β}
:
Set.Infinite s → Set.Infinite (a • s)
Alias of the reverse direction of Set.infinite_smul_set
.
theorem
Set.Finite.of_vadd_set
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddAction α β]
{a : α}
{s : Set β}
:
Set.Finite (a +ᵥ s) → Set.Finite s
theorem
Set.Infinite.vadd_set
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddAction α β]
{a : α}
{s : Set β}
:
Set.Infinite s → Set.Infinite (a +ᵥ s)
theorem
AddGroup.card_nsmul_eq_card_nsmul_card_univ
{G : Type u_5}
[AddGroup G]
[Fintype G]
(S : Set G)
[(k : ℕ) → DecidablePred fun x => x ∈ k • S]
(k : ℕ)
:
Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)
theorem
Group.card_pow_eq_card_pow_card_univ
{G : Type u_5}
[Group G]
[Fintype G]
(S : Set G)
[(k : ℕ) → DecidablePred fun x => x ∈ S ^ k]
(k : ℕ)
:
Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)