Finiteness lemmas for pointwise operations on sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
set.fintype_add
{α : Type u_2}
[has_add α]
[decidable_eq α]
(s t : set α)
[fintype ↥s]
[fintype ↥t] :
Addition preserves finiteness.
Equations
- s.fintype_add t = set.fintype_image2 (λ (a b : α), a + b) s t
def
set.fintype_mul
{α : Type u_2}
[has_mul α]
[decidable_eq α]
(s t : set α)
[fintype ↥s]
[fintype ↥t] :
Multiplication preserves finiteness.
Equations
- s.fintype_mul t = set.fintype_image2 (λ (a b : α), a * b) s t
@[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)
@[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)
@[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
- set.decidable_mem_nsmul n = 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 : α), set.decidable_mem_add 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
- set.decidable_mem_pow n = 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 : α), set.decidable_mem_mul a)) n
theorem
set.finite.of_smul_set
{α : Type u_2}
{β : Type u_3}
[group α]
[mul_action α β]
{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 α]
[mul_action α β]
{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 α]
[add_action α β]
{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 α]
[add_action α β]
{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 : ℕ) :
fintype.card G ≤ k → fintype.card ↥(S ^ k) = fintype.card ↥(S ^ fintype.card G)
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 : ℕ) :
fintype.card G ≤ k → fintype.card ↥(k • S) = fintype.card ↥(fintype.card G • S)