Documentation

@[implicit_reducible]

instance Set.decidableMemAdd {α : Type u_2} [AddMonoid α] {s t : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : α) => x ∈ t] :

DecidablePred fun (x : α) => x ∈ s + t

@[implicit_reducible]

instance Set.decidableMemPow {α : Type u_2} [Monoid α] {s : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x ∈ s] (n : ℕ) :

DecidablePred fun (x : α) => x ∈ s ^ n

@[implicit_reducible]

instance Set.decidableMemNSMul {α : Type u_2} [AddMonoid α] {s : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x ∈ s] (n : ℕ) :

DecidablePred fun (x : α) => x ∈ n • s

theorem Set.Finite.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :

s.Finite → t.Finite → (s • t).Finite

theorem Set.Finite.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :

s.Finite → t.Finite → (s +ᵥ t).Finite

theorem Set.Finite.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :

s.Finite → (a • s).Finite

theorem Set.Finite.vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :

s.Finite → (a +ᵥ s).Finite

theorem Set.Infinite.of_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} :

(a • s).Infinite → s.Infinite

theorem Set.Infinite.of_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} :

(a +ᵥ s).Infinite → s.Infinite

theorem Set.Finite.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s t : Set β} (hs : s.Finite) (ht : t.Finite) :

(s -ᵥ t).Finite

theorem Set.finite_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s t : Set α} :

(s * t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

theorem Set.finite_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s t : Set α} :

(s + t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

theorem Set.infinite_mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s t : Set α} :

(s * t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

theorem Set.infinite_add {α : Type u_2} [Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s t : Set α} :

(s + t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

@[simp]

theorem Set.finite_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :

s⁻¹.Finite ↔ s.Finite

@[simp]

theorem Set.finite_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :

(-s).Finite ↔ s.Finite

@[simp]

theorem Set.infinite_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :

s⁻¹.Infinite ↔ s.Infinite

@[simp]

theorem Set.infinite_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :

(-s).Infinite ↔ s.Infinite

theorem Set.Finite.of_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :

s⁻¹.Finite → s.Finite

Alias of the forward direction of Set.finite_inv.

theorem Set.Finite.inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :

s.Finite → s⁻¹.Finite

Alias of the reverse direction of Set.finite_inv.

theorem Set.Finite.of_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :

(-s).Finite → s.Finite

theorem Set.Finite.neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :

s.Finite → (-s).Finite

theorem Set.Finite.div {α : Type u_2} [Div α] {s t : Set α} :

s.Finite → t.Finite → (s / t).Finite

theorem Set.Finite.sub {α : Type u_2} [Sub α] {s t : Set α} :

s.Finite → t.Finite → (s - t).Finite

@[implicit_reducible]

instance Set.fintypeDiv {α : Type u_2} [Div α] [DecidableEq α] (s t : Set α) [Fintype ↑s] [Fintype ↑t] :

Fintype ↑(s / t)

Division preserves finiteness.

@[implicit_reducible]

instance Set.fintypeSub {α : Type u_2} [Sub α] [DecidableEq α] (s t : Set α) [Fintype ↑s] [Fintype ↑t] :

Fintype ↑(s - t)

Subtraction preserves finiteness.

theorem Set.finite_div {α : Type u_2} [Group α] {s t : Set α} :

(s / t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

theorem Set.finite_sub {α : Type u_2} [AddGroup α] {s t : Set α} :

(s - t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

theorem Set.infinite_div {α : Type u_2} [Group α] {s t : Set α} :

(s / t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

theorem Set.infinite_sub {α : Type u_2} [AddGroup α] {s t : Set α} :

(s - t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

theorem Group.card_pow_eq_card_pow_card_univ {G : Type u_5} [Group G] [Fintype G] (S : Set G) [(k : ℕ) → DecidablePred fun (x : G) => x ∈ S ^ k] (k : ℕ) :

Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)