Documentation

Mathlib.Data.Set.Pointwise.Finite

Finiteness lemmas for pointwise operations on sets #

theorem Set.Finite.neg {α : Type u_1} [inst : InvolutiveNeg α] {s : Set α} (hs : Set.Finite s) :
theorem Set.Finite.inv {α : Type u_1} [inst : InvolutiveInv α] {s : Set α} (hs : Set.Finite s) :
theorem Set.Finite.add {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
Set.Finite sSet.Finite tSet.Finite (s + t)
theorem Set.Finite.mul {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
Set.Finite sSet.Finite tSet.Finite (s * t)
def Set.fintypeAdd {α : Type u_1} [inst : Add α] [inst : DecidableEq α] (s : Set α) (t : Set α) [inst : Fintype s] [inst : Fintype t] :
Fintype ↑(s + t)

Addition preserves finiteness.

Equations
def Set.fintypeMul {α : Type u_1} [inst : Mul α] [inst : DecidableEq α] (s : Set α) (t : Set α) [inst : Fintype s] [inst : Fintype t] :
Fintype ↑(s * t)

Multiplication preserves finiteness.

Equations
def Set.decidableMemAdd.proof_1 {α : Type u_1} [inst : AddMonoid α] {s : Set α} {t : Set α} :
∀ (x : α), (x_1 y, x_1 s y t x_1 + y = x) x s + t
Equations
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
Equations
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
Equations
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
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
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 β} :
theorem Set.Finite.smul {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s : Set α} {t : Set β} :
theorem Set.Finite.vadd_set {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α} :
theorem Set.Finite.smul_set {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α} :
theorem Set.Finite.vsub {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s : Set β} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) :
abbrev AddGroup.card_nsmul_eq_card_nsmul_card_univ.match_1 {G : Type u_1} (s : Set G) (motive : sSort u_2) :
(x : s) → ((b : G) → (hb : b s) → motive { val := b, property := hb }) → motive x
Equations
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 : ) :
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 : ) :