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)
def
Set.fintypeAdd
{α : Type u_2}
[Add α]
[DecidableEq α]
(s : Set α)
(t : Set α)
[Fintype ↑s]
[Fintype ↑t]
:
Addition preserves finiteness.
Equations
- Set.fintypeAdd s t = Set.fintypeImage2 (fun (x x_1 : α) => x + x_1) s t
Instances For
def
Set.fintypeMul
{α : Type u_2}
[Mul α]
[DecidableEq α]
(s : Set α)
(t : Set α)
[Fintype ↑s]
[Fintype ↑t]
:
Multiplication preserves finiteness.
Equations
- Set.fintypeMul s t = Set.fintypeImage2 (fun (x x_1 : α) => x * x_1) s t
Instances For
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
Equations
- Set.decidableMemAdd x = decidable_of_iff (∃ x_1 ∈ s, ∃ y ∈ t, x_1 + y = x) ⋯
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
Equations
- Set.decidableMemMul x = decidable_of_iff (∃ x_1 ∈ s, ∃ y ∈ t, x_1 * y = x) ⋯
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 ∈ n • s + s
instance
Set.decidableMemNSMul
{α : Type u_2}
[AddMonoid α]
{s : Set α}
[Fintype α]
[DecidableEq α]
[DecidablePred fun (x : α) => x ∈ s]
(n : ℕ)
:
DecidablePred fun (x : α) => x ∈ n • s
Equations
- Set.decidableMemNSMul n = Nat.rec (Eq.mpr ⋯ inferInstance) (fun (n : ℕ) (ih : DecidablePred fun (x : α) => x ∈ n • s) => Eq.mpr ⋯ inferInstance) n
instance
Set.decidableMemPow
{α : Type u_2}
[Monoid α]
{s : Set α}
[Fintype α]
[DecidableEq α]
[DecidablePred fun (x : α) => x ∈ s]
(n : ℕ)
:
DecidablePred fun (x : α) => x ∈ s ^ n
Equations
- Set.decidableMemPow n = Nat.rec (Eq.mpr ⋯ inferInstance) (fun (n : ℕ) (ih : DecidablePred fun (x : α) => x ∈ s ^ n) => Eq.mpr ⋯ inferInstance) 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
theorem
Set.finite_add
{α : Type u_2}
[Add α]
[IsLeftCancelAdd α]
[IsRightCancelAdd α]
{s : Set α}
{t : Set α}
:
Set.Finite (s + t) ↔ Set.Finite s ∧ Set.Finite t ∨ s = ∅ ∨ t = ∅
theorem
Set.finite_mul
{α : Type u_2}
[Mul α]
[IsLeftCancelMul α]
[IsRightCancelMul α]
{s : Set α}
{t : Set α}
:
Set.Finite (s * t) ↔ Set.Finite s ∧ Set.Finite t ∨ s = ∅ ∨ t = ∅
@[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.Infinite.vadd_set
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddAction α β]
{a : α}
{s : Set β}
:
Set.Infinite s → Set.Infinite (a +ᵥ s)
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
AddGroup.card_nsmul_eq_card_nsmul_card_univ
{G : Type u_5}
[AddGroup G]
[Fintype G]
(S : Set G)
[(k : ℕ) → DecidablePred fun (x : G) => x ∈ k • S]
(k : ℕ)
:
Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)
abbrev
AddGroup.card_nsmul_eq_card_nsmul_card_univ.match_1
{G : Type u_1}
(s : Set G)
(motive : ↑s → Sort u_2)
:
(x : ↑s) → ((b : G) → (hb : b ∈ s) → motive { val := b, property := hb }) → motive x
Equations
- AddGroup.card_nsmul_eq_card_nsmul_card_univ.match_1 s motive x h_1 = Subtype.casesOn x fun (val : G) (property : val ∈ s) => h_1 val property
Instances For
theorem
Group.card_pow_eq_card_pow_card_univ
{G : Type u_5}
[Group G]
[Fintype G]
(S : Set G)
[(k : ℕ) → DecidablePred fun (x : G) => x ∈ S ^ k]
(k : ℕ)
:
Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)