mathlib3 documentation

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.

source
@[simp]
theorem set.finite_one {α : Type u_2} [has_one α] :
1.finite
source
@[simp]
theorem set.finite_zero {α : Type u_2} [has_zero α] :
0.finite
source
theorem set.finite.inv {α : Type u_2} [has_involutive_inv α] {s : set α} (hs : s.finite) :
s⁻¹.finite
source
theorem set.finite.neg {α : Type u_2} [has_involutive_neg α] {s : set α} (hs : s.finite) :
(-s).finite
source
theorem set.finite.mul {α : Type u_2} [has_mul α] {s t : set α} :
s.finite → t.finite → (s * t).finite
source
theorem set.finite.add {α : Type u_2} [has_add α] {s t : set α} :
s.finite → t.finite → (s + t).finite
source
def set.fintype_add {α : Type u_2} [has_add α] [decidable_eq α] (s t : set α) [fintype ↥s] [fintype ↥t] :
fintype ↥(s + t)

Addition preserves finiteness.

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

Multiplication preserves finiteness.

Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem set.finite.smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
s.finite → t.finite → (s • t).finite
source
theorem set.finite.vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
s.finite → t.finite → (s +ᵥ t).finite
source
theorem set.finite.vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :
s.finite → (a +ᵥ s).finite
source
theorem set.finite.smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
s.finite → (a • s).finite
source
theorem set.infinite.of_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
(a • s).infinite → s.infinite
source
theorem set.infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :
(a +ᵥ s).infinite → s.infinite
source
theorem set.finite.vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} (hs : s.finite) (ht : t.finite) :
(s -ᵥ t).finite
source
theorem set.infinite_mul {α : Type u_2} [has_mul α] [is_left_cancel_mul α] [is_right_cancel_mul α] {s t : set α} :
(s * t).infinite ↔ s.infinite ∧ t.nonempty ∨ t.infinite ∧ s.nonempty
source
theorem set.infinite_add {α : Type u_2} [has_add α] [is_left_cancel_add α] [is_right_cancel_add α] {s t : set α} :
(s + t).infinite ↔ s.infinite ∧ t.nonempty ∨ t.infinite ∧ s.nonempty
source
@[simp]
theorem set.finite_smul_set {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} {s : set β} :
(a • s).finite ↔ s.finite
source
@[simp]
theorem set.finite_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} {s : set β} :
(a +ᵥ s).finite ↔ s.finite
source
@[simp]
theorem set.infinite_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} {s : set β} :
(a +ᵥ s).infinite ↔ s.infinite
source
@[simp]
theorem set.infinite_smul_set {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} {s : set β} :
(a • s).infinite ↔ s.infinite
source
theorem set.finite.of_smul_set {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} {s : set β} :
(a • s).finite → s.finite

Alias of the forward direction of set.finite_smul_set.

source
theorem set.infinite.smul_set {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} {s : set β} :
s.infinite → (a • s).infinite

Alias of the reverse direction of set.infinite_smul_set.

source
theorem set.infinite.vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} {s : set β} :
s.infinite → (a +ᵥ s).infinite

Alias of the reverse direction of set.infinite_smul_set.

source
theorem set.finite.of_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} {s : set β} :
(a +ᵥ s).finite → s.finite

Alias of the forward direction of set.finite_smul_set.

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