# mathlib3documentation

data.set.pointwise.finite

# Finiteness lemmas for pointwise operations on sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp]
theorem set.finite_one {α : Type u_2} [has_one α] :
@[simp]
theorem set.finite_zero {α : Type u_2} [has_zero α] :
theorem set.finite.inv {α : Type u_2} {s : set α} (hs : s.finite) :
theorem set.finite.neg {α : Type u_2} {s : set α} (hs : s.finite) :
theorem set.finite.mul {α : Type u_2} [has_mul α] {s t : set α} :
theorem set.finite.add {α : Type u_2} [has_add α] {s t : set α} :
def set.fintype_add {α : Type u_2} [has_add α] [decidable_eq α] (s t : set α) [fintype s] [fintype t] :

Equations
def set.fintype_mul {α : Type u_2} [has_mul α] [decidable_eq α] (s t : set α) [fintype s] [fintype t] :

Multiplication preserves finiteness.

Equations
@[protected, instance]
def set.decidable_mem_add {α : Type u_2} [add_monoid α] {s t : set α} [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x s)] [decidable_pred (λ (_x : α), _x t)] :
decidable_pred (λ (_x : α), _x s + t)
Equations
@[protected, instance]
def set.decidable_mem_mul {α : Type u_2} [monoid α] {s t : set α} [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x s)] [decidable_pred (λ (_x : α), _x t)] :
decidable_pred (λ (_x : α), _x s * t)
Equations
@[protected, instance]
def set.decidable_mem_nsmul {α : Type u_2} [add_monoid α] {s : set α} [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x s)] (n : ) :
decidable_pred (λ (_x : α), _x n s)
Equations
• = nat.rec (set.decidable_mem_nsmul._proof_1.mpr (set.decidable_mem_nsmul._proof_2.mpr (λ (a : α), _inst_3 a 0))) (λ (n : ) (ih : decidable_pred (λ (_x : α), _x n s)), let _inst : decidable_pred (λ (_x : α), _x n s) := ih in _.mpr (λ (a : α), n
@[protected, instance]
def set.decidable_mem_pow {α : Type u_2} [monoid α] {s : set α} [fintype α] [decidable_eq α] [decidable_pred (λ (_x : α), _x s)] (n : ) :
decidable_pred (λ (_x : α), _x s ^ n)
Equations
• = nat.rec (set.decidable_mem_pow._proof_1.mpr (set.decidable_mem_pow._proof_2.mpr (λ (a : α), _inst_3 a 1))) (λ (n : ) (ih : decidable_pred (λ (_x : α), _x s ^ n)), let _inst : decidable_pred (λ (_x : α), _x s ^ n) := ih in _.mpr (λ (a : α), n
theorem set.finite.smul {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.finite.vadd {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.finite.vadd_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
theorem set.finite.smul_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
theorem set.infinite.of_smul_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
theorem set.infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
theorem set.finite.vsub {α : Type u_2} {β : Type u_3} [ β] {s t : set β} (hs : s.finite) (ht : t.finite) :
(s -ᵥ t).finite
theorem set.infinite_mul {α : Type u_2} [has_mul α] {s t : set α} :
(s * t).infinite
theorem set.infinite_add {α : Type u_2} [has_add α] {s t : set α} :
(s + t).infinite
@[simp]
theorem set.finite_smul_set {α : Type u_2} {β : Type u_3} [group α] [ β] {a : α} {s : set β} :
@[simp]
theorem set.finite_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [ β] {a : α} {s : set β} :
@[simp]
theorem set.infinite_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [ β] {a : α} {s : set β} :
@[simp]
theorem set.infinite_smul_set {α : Type u_2} {β : Type u_3} [group α] [ β] {a : α} {s : set β} :
theorem set.finite.of_smul_set {α : Type u_2} {β : Type u_3} [group α] [ β] {a : α} {s : set β} :

Alias of the forward direction of set.finite_smul_set.

theorem set.infinite.smul_set {α : Type u_2} {β : Type u_3} [group α] [ β] {a : α} {s : set β} :

Alias of the reverse direction of set.infinite_smul_set.

theorem set.infinite.vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [ β] {a : α} {s : set β} :

Alias of the reverse direction of set.infinite_smul_set.

theorem set.finite.of_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [ β] {a : α} {s : set β} :

Alias of the forward direction of set.finite_smul_set.

theorem group.card_pow_eq_card_pow_card_univ {G : Type u_5} [group G] [fintype G] (S : set G) [Π (k : ), decidable_pred (λ (_x : G), _x S ^ k)] (k : ) :
theorem add_group.card_nsmul_eq_card_nsmul_card_univ {G : Type u_5} [add_group G] [fintype G] (S : set G) [Π (k : ), decidable_pred (λ (_x : G), _x k S)] (k : ) :