Finiteness lemmas for pointwise operations on sets #

@[simp]
theorem Set.finite_zero {α : Type u_2} [Zero α] :
@[simp]
theorem Set.finite_one {α : Type u_2} [One α] :
theorem Set.Finite.neg {α : Type u_2} [] {s : Set α} (hs : s.Finite) :
(-s).Finite
theorem Set.Finite.inv {α : Type u_2} [] {s : Set α} (hs : s.Finite) :
s⁻¹.Finite
theorem Set.Finite.add {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
s.Finitet.Finite(s + t).Finite
theorem Set.Finite.mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
s.Finitet.Finite(s * t).Finite
def Set.fintypeAdd {α : Type u_2} [Add α] [] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
Fintype (s + t)

Equations
Instances For
def Set.fintypeMul {α : Type u_2} [Mul α] [] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
Fintype (s * t)

Multiplication preserves finiteness.

Equations
Instances For
instance Set.decidableMemAdd {α : Type u_2} [] {s : Set α} {t : Set α} [] [] [DecidablePred fun (x : α) => x s] [DecidablePred fun (x : α) => x t] :
DecidablePred fun (x : α) => x s + t
Equations
theorem Set.decidableMemAdd.proof_1 {α : Type u_1} [] {s : Set α} {t : Set α} :
∀ (x : α), (x_1s, yt, x_1 + y = x) x s + t
instance Set.decidableMemMul {α : Type u_2} [] {s : Set α} {t : Set α} [] [] [DecidablePred fun (x : α) => x s] [DecidablePred fun (x : α) => x t] :
DecidablePred fun (x : α) => x s * t
Equations
theorem Set.decidableMemNSMul.proof_1 {α : Type u_1} [] {s : Set α} :
(DecidablePred fun (x : α) => x 0 s) = DecidablePred fun (x : α) => x = 0
theorem Set.decidableMemNSMul.proof_2 {α : Type u_1} [] {s : Set α} (n : ) :
(DecidablePred fun (x : α) => x (n + 1) s) = DecidablePred fun (x : α) => x n s + s
instance Set.decidableMemNSMul {α : Type u_2} [] {s : Set α} [] [] [DecidablePred fun (x : α) => x s] (n : ) :
DecidablePred fun (x : α) => x n s
Equations
instance Set.decidableMemPow {α : Type u_2} [] {s : Set α} [] [] [DecidablePred fun (x : α) => x s] (n : ) :
DecidablePred fun (x : α) => x s ^ n
Equations
theorem Set.Finite.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
s.Finitet.Finite(s +ᵥ t).Finite
theorem Set.Finite.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
s.Finitet.Finite(s t).Finite
theorem Set.Finite.vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :
s.Finite(a +ᵥ s).Finite
theorem Set.Finite.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
s.Finite(a s).Finite
theorem Set.Infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :
(a +ᵥ s).Infinites.Infinite
theorem Set.Infinite.of_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :
(a s).Infinites.Infinite
theorem Set.Finite.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
(s -ᵥ t).Finite
theorem Set.infinite_add {α : Type u_2} [Add α] [] [] {s : Set α} {t : Set α} :
(s + t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
theorem Set.infinite_mul {α : Type u_2} [Mul α] [] [] {s : Set α} {t : Set α} :
(s * t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
theorem Set.finite_add {α : Type u_2} [Add α] [] [] {s : Set α} {t : Set α} :
(s + t).Finite s.Finite t.Finite s = t =
theorem Set.finite_mul {α : Type u_2} [Mul α] [] [] {s : Set α} {t : Set α} :
(s * t).Finite s.Finite t.Finite s = t =
@[simp]
theorem Set.finite_vadd_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
(a +ᵥ s).Finite s.Finite
@[simp]
theorem Set.finite_smul_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
(a s).Finite s.Finite
@[simp]
theorem Set.infinite_vadd_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
(a +ᵥ s).Infinite s.Infinite
@[simp]
theorem Set.infinite_smul_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
(a s).Infinite s.Infinite
theorem Set.Finite.of_smul_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
(a s).Finites.Finite

Alias of the forward direction of Set.finite_smul_set.

theorem Set.Infinite.smul_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
s.Infinite(a s).Infinite

Alias of the reverse direction of Set.infinite_smul_set.

theorem Set.Infinite.vadd_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
s.Infinite(a +ᵥ s).Infinite
theorem Set.Finite.of_vadd_set {α : Type u_2} {β : Type u_3} [] [] {a : α} {s : Set β} :
(a +ᵥ s).Finites.Finite
theorem AddGroup.card_nsmul_eq_card_nsmul_card_univ {G : Type u_5} [] [] (S : Set G) [(k : ) → DecidablePred fun (x : G) => x k S] (k : ) :
Fintype.card (k S) = Fintype.card ()
abbrev AddGroup.card_nsmul_eq_card_nsmul_card_univ.match_1 {G : Type u_1} (s : Set G) (motive : sSort u_2) :
(x : s) → ((b : G) → (hb : b s) → motive b, hb)motive x
Equations
Instances For
theorem Group.card_pow_eq_card_pow_card_univ {G : Type u_5} [] [] (S : Set G) [(k : ) → DecidablePred fun (x : G) => x S ^ k] (k : ) :
Fintype.card (S ^ k) = Fintype.card ()