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.

@[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} [has_involutive_inv α] {s : set α} (hs : s.finite) :
theorem set.finite.neg {α : Type u_2} [has_involutive_neg α] {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] :

Addition preserves finiteness.

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
@[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
theorem set.finite.smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
theorem set.finite.vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
theorem set.finite.vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :
theorem set.finite.smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
theorem set.infinite.of_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
theorem set.infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :
theorem set.finite.vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} (hs : s.finite) (ht : t.finite) :
(s -ᵥ t).finite
@[simp]
theorem set.finite_smul_set {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} {s : set β} :
@[simp]
theorem set.finite_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} {s : set β} :
@[simp]
theorem set.infinite_vadd_set {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} {s : set β} :
@[simp]
theorem set.infinite_smul_set {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} {s : set β} :
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 : ) :
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 : ) :