Finiteness lemmas for pointwise operations on sets #
theorem
Set.Finite.neg
{α : Type u_1}
[inst : InvolutiveNeg α]
{s : Set α}
(hs : Set.Finite s)
:
Set.Finite (-s)
theorem
Set.Finite.add
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
Set.Finite s → Set.Finite t → Set.Finite (s + t)
theorem
Set.Finite.mul
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
Set.Finite s → Set.Finite t → Set.Finite (s * t)
def
Set.fintypeAdd
{α : Type u_1}
[inst : Add α]
[inst : DecidableEq α]
(s : Set α)
(t : Set α)
[inst : Fintype ↑s]
[inst : Fintype ↑t]
:
Addition preserves finiteness.
Equations
- Set.fintypeAdd s t = Set.fintypeImage2 (fun x x_1 => x + x_1) s t
def
Set.fintypeMul
{α : Type u_1}
[inst : Mul α]
[inst : DecidableEq α]
(s : Set α)
(t : Set α)
[inst : Fintype ↑s]
[inst : Fintype ↑t]
:
Multiplication preserves finiteness.
Equations
- Set.fintypeMul s t = Set.fintypeImage2 (fun x x_1 => x * x_1) s t
instance
Set.decidableMemAdd
{α : Type u_1}
[inst : AddMonoid α]
{s : Set α}
{t : Set α}
[inst : Fintype α]
[inst : DecidableEq α]
[inst : DecidablePred fun x => x ∈ s]
[inst : DecidablePred fun x => x ∈ t]
:
DecidablePred fun x => x ∈ s + t
instance
Set.decidableMemMul
{α : Type u_1}
[inst : Monoid α]
{s : Set α}
{t : Set α}
[inst : Fintype α]
[inst : DecidableEq α]
[inst : DecidablePred fun x => x ∈ s]
[inst : DecidablePred fun x => x ∈ t]
:
DecidablePred fun x => x ∈ s * t
def
Set.decidableMemNSMul.proof_2
{α : Type u_1}
[inst : AddMonoid α]
{s : Set α}
(n : ℕ)
:
(DecidablePred fun x => x ∈ Nat.succ n • s) = DecidablePred fun x => x ∈ s + n • s
Equations
- (_ : (DecidablePred fun x => x ∈ Nat.succ n • s) = DecidablePred fun x => x ∈ s + n • s) = (_ : (DecidablePred fun x => x ∈ Nat.succ n • s) = DecidablePred fun x => x ∈ s + n • s)
instance
Set.decidableMemNSMul
{α : Type u_1}
[inst : AddMonoid α]
{s : Set α}
[inst : Fintype α]
[inst : DecidableEq α]
[inst : DecidablePred fun x => x ∈ s]
(n : ℕ)
:
DecidablePred fun x => x ∈ n • s
Equations
- One or more equations did not get rendered due to their size.
def
Set.decidableMemNSMul.proof_1
{α : Type u_1}
[inst : AddMonoid α]
{s : Set α}
:
(DecidablePred fun x => x ∈ Nat.zero • s) = DecidablePred fun x => x = 0
Equations
- (_ : (DecidablePred fun x => x ∈ Nat.zero • s) = DecidablePred fun x => x = 0) = (_ : (DecidablePred fun x => x ∈ Nat.zero • s) = DecidablePred fun x => x = 0)
instance
Set.decidableMemPow
{α : Type u_1}
[inst : Monoid α]
{s : Set α}
[inst : Fintype α]
[inst : DecidableEq α]
[inst : DecidablePred fun x => x ∈ s]
(n : ℕ)
:
DecidablePred fun x => x ∈ s ^ n
Equations
- One or more equations did not get rendered due to their size.
theorem
Set.Finite.vadd
{α : Type u_1}
{β : Type u_2}
[inst : VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Finite s → Set.Finite t → Set.Finite (s +ᵥ t)
theorem
Set.Finite.smul
{α : Type u_1}
{β : Type u_2}
[inst : 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_1}
[inst : VAdd α β]
{s : Set β}
{a : α}
:
Set.Finite s → Set.Finite (a +ᵥ s)
theorem
Set.Finite.smul_set
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set β}
{a : α}
:
Set.Finite s → Set.Finite (a • s)
theorem
Set.Finite.vsub
{α : Type u_2}
{β : Type u_1}
[inst : VSub α β]
{s : Set β}
{t : Set β}
(hs : Set.Finite s)
(ht : Set.Finite t)
:
Set.Finite (s -ᵥ t)
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 property => h_1 val property
theorem
AddGroup.card_nsmul_eq_card_nsmul_card_univ
{G : Type u_1}
[inst : AddGroup G]
[inst : Fintype G]
(S : Set G)
[inst : (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_1}
[inst : Group G]
[inst : Fintype G]
(S : Set G)
[inst : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k]
(k : ℕ)
:
Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)