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) :

Set.Finite (-s)

theorem Set.Finite.inv {α : Type u_1} [inst : InvolutiveInv α] {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] :

Fintype ↑(s + 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] :

Fintype ↑(s * t)

Multiplication preserves finiteness.

Equations

Set.fintypeMul s t = Set.fintypeImage2 (fun x x_1 => x * x_1) s t

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

(_ : (∃ x y, x ∈ s ∧ y ∈ t ∧ x + y = x) ↔ x ∈ s + t) = (_ : (∃ x y, x ∈ s ∧ y ∈ t ∧ x + y = x) ↔ x ∈ 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

Equations

Set.decidableMemAdd x = decidable_of_iff (∃ x y, x ∈ s ∧ y ∈ t ∧ x + y = x) (_ : (∃ x y, x ∈ s ∧ y ∈ t ∧ x + y = 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

Equations

Set.decidableMemMul x = decidable_of_iff (∃ x y, x ∈ s ∧ y ∈ t ∧ x * y = x) (_ : (∃ x y, x ∈ s ∧ y ∈ t ∧ x * y = 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)