Pointwise operations of sets #
This file defines pointwise algebraic operations on sets.
Main declarations #
For sets s and t and scalar a:
s * t: Multiplication, set of allx * ywherex ∈ s∈ sandy ∈ t∈ t.s + t: Addition, set of allx + ywherex ∈ s∈ sandy ∈ t∈ t.s⁻¹⁻¹: Inversion, set of allx⁻¹⁻¹wherex ∈ s∈ s.-s: Negation, set of all-xwherex ∈ s∈ s.s / t: Division, set of allx / ywherex ∈ s∈ sandy ∈ t∈ t.s - t: Subtraction, set of allx - ywherex ∈ s∈ sandy ∈ t∈ t.
For α a semigroup/monoid, Set α is a semigroup/monoid.
As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between
pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while
the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}. See note [pointwise nat action].
Appropriate definitions and results are also transported to the additive theory via to_additive.
Implementation notes #
- The following expressions are considered in simp-normal form in a group:
(λ h, h * g) ⁻¹' s⁻¹' s,(λ h, g * h) ⁻¹' s⁻¹' s,(λ h, h * g⁻¹) ⁻¹' s⁻¹) ⁻¹' s⁻¹' s,(λ h, g⁻¹ * h) ⁻¹' s⁻¹ * h) ⁻¹' s⁻¹' s,s * t,s⁻¹⁻¹,(1 : Set _)(and similarly for additive variants). Expressions equal to one of these will be simplified. - We put all instances in the locale
Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior ofsimp.
Tags #
set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction
0/1 as sets #
theorem
Set.Nonempty.subset_zero_iff
{α : Type u_1}
[inst : Zero α]
{s : Set α}
(h : Set.Nonempty s)
:
theorem
Set.Nonempty.subset_one_iff
{α : Type u_1}
[inst : One α]
{s : Set α}
(h : Set.Nonempty s)
:
Set negation/inversion #
The pointwise negation of set -s is defined as {x | -x ∈ s}∈ s} in locale Pointwise.
It is equal to {-x | x ∈ s}∈ s}, see Set.image_neg.
Equations
- Set.neg = { neg := Set.preimage Neg.neg }
The pointwise inversion of set s⁻¹⁻¹ is defined as {x | x⁻¹ ∈ s}⁻¹ ∈ s}∈ s} in locale Pointwise. It is
equal to {x⁻¹ | x ∈ s}⁻¹ | x ∈ s}∈ s}, see Set.image_inv.
Equations
- Set.inv = { inv := Set.preimage Inv.inv }
@[simp]
theorem
Set.interᵢ_neg
{α : Type u_1}
{ι : Sort u_2}
[inst : Neg α]
(s : ι → Set α)
:
(-Set.interᵢ fun i => s i) = Set.interᵢ fun i => -s i
@[simp]
theorem
Set.interᵢ_inv
{α : Type u_1}
{ι : Sort u_2}
[inst : Inv α]
(s : ι → Set α)
:
(Set.interᵢ fun i => s i)⁻¹ = Set.interᵢ fun i => (s i)⁻¹
@[simp]
theorem
Set.unionᵢ_neg
{α : Type u_1}
{ι : Sort u_2}
[inst : Neg α]
(s : ι → Set α)
:
(-Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => -s i
@[simp]
theorem
Set.unionᵢ_inv
{α : Type u_1}
{ι : Sort u_2}
[inst : Inv α]
(s : ι → Set α)
:
(Set.unionᵢ fun i => s i)⁻¹ = Set.unionᵢ fun i => (s i)⁻¹
@[simp]
theorem
Set.nonempty_neg
{α : Type u_1}
[inst : InvolutiveNeg α]
{s : Set α}
:
Set.Nonempty (-s) ↔ Set.Nonempty s
@[simp]
theorem
Set.Nonempty.neg
{α : Type u_1}
[inst : InvolutiveNeg α]
{s : Set α}
(h : Set.Nonempty s)
:
Set.Nonempty (-s)
@[simp]
@[simp]
noncomputable instance
Set.involutiveNeg
{α : Type u_1}
[inst : InvolutiveNeg α]
:
InvolutiveNeg (Set α)
noncomputable instance
Set.involutiveInv
{α : Type u_1}
[inst : InvolutiveInv α]
:
InvolutiveInv (Set α)
@[simp]
@[simp]
Set addition/multiplication #
@[simp]
theorem
Set.add_nonempty
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s + t) ↔ Set.Nonempty s ∧ Set.Nonempty t
@[simp]
theorem
Set.mul_nonempty
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s * t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.add
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s + t)
theorem
Set.Nonempty.mul
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s * t)
theorem
Set.Nonempty.of_add_left
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s + t) → Set.Nonempty s
theorem
Set.Nonempty.of_mul_left
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s * t) → Set.Nonempty s
theorem
Set.Nonempty.of_add_right
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s + t) → Set.Nonempty t
theorem
Set.Nonempty.of_mul_right
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s * t) → Set.Nonempty t
theorem
Set.unionᵢ_add_left_image
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x x_1 => x + x_1) a '' t) = s + t
theorem
Set.unionᵢ_mul_left_image
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x x_1 => x * x_1) a '' t) = s * t
theorem
Set.unionᵢ_add_right_image
{α : Type u_1}
[inst : Add α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x + a) '' s) = s + t
theorem
Set.unionᵢ_mul_right_image
{α : Type u_1}
[inst : Mul α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x * a) '' s) = s * t
theorem
Set.unionᵢ_add
{α : Type u_1}
{ι : Sort u_2}
[inst : Add α]
(s : ι → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => s i) + t = Set.unionᵢ fun i => s i + t
theorem
Set.unionᵢ_mul
{α : Type u_1}
{ι : Sort u_2}
[inst : Mul α]
(s : ι → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => s i) * t = Set.unionᵢ fun i => s i * t
theorem
Set.add_unionᵢ
{α : Type u_1}
{ι : Sort u_2}
[inst : Add α]
(s : Set α)
(t : ι → Set α)
:
(s + Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s + t i
theorem
Set.mul_unionᵢ
{α : Type u_1}
{ι : Sort u_2}
[inst : Mul α]
(s : Set α)
(t : ι → Set α)
:
(s * Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s * t i
theorem
Set.unionᵢ₂_add
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Add α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) + t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j + t
theorem
Set.unionᵢ₂_mul
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Mul α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) * t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j * t
theorem
Set.add_unionᵢ₂
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Add α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s + Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s + t i j
theorem
Set.mul_unionᵢ₂
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Mul α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s * Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s * t i j
theorem
Set.interᵢ_add_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Add α]
(s : ι → Set α)
(t : Set α)
:
(Set.interᵢ fun i => s i) + t ⊆ Set.interᵢ fun i => s i + t
theorem
Set.interᵢ_mul_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Mul α]
(s : ι → Set α)
(t : Set α)
:
(Set.interᵢ fun i => s i) * t ⊆ Set.interᵢ fun i => s i * t
theorem
Set.add_interᵢ_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Add α]
(s : Set α)
(t : ι → Set α)
:
(s + Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s + t i
theorem
Set.mul_interᵢ_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Mul α]
(s : Set α)
(t : ι → Set α)
:
(s * Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s * t i
theorem
Set.interᵢ₂_add_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Add α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) + t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j + t
theorem
Set.interᵢ₂_mul_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Mul α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) * t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j * t
theorem
Set.add_interᵢ₂_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Add α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s + Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s + t i j
theorem
Set.mul_interᵢ₂_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Mul α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s * Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s * t i j
Set subtraction/division #
@[simp]
theorem
Set.image2_sub
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
Set.image2 Sub.sub s t = s - t
@[simp]
theorem
Set.image2_div
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
Set.image2 Div.div s t = s / t
@[simp]
theorem
Set.sub_nonempty
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s - t) ↔ Set.Nonempty s ∧ Set.Nonempty t
@[simp]
theorem
Set.div_nonempty
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s / t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.sub
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s - t)
theorem
Set.Nonempty.div
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s / t)
theorem
Set.Nonempty.of_sub_left
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s - t) → Set.Nonempty s
theorem
Set.Nonempty.of_div_left
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s / t) → Set.Nonempty s
theorem
Set.Nonempty.of_sub_right
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s - t) → Set.Nonempty t
theorem
Set.Nonempty.of_div_right
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s / t) → Set.Nonempty t
theorem
Set.unionᵢ_sub_left_image
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x x_1 => x - x_1) a '' t) = s - t
theorem
Set.unionᵢ_div_left_image
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x x_1 => x / x_1) a '' t) = s / t
theorem
Set.unionᵢ_sub_right_image
{α : Type u_1}
[inst : Sub α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x - a) '' s) = s - t
theorem
Set.unionᵢ_div_right_image
{α : Type u_1}
[inst : Div α]
{s : Set α}
{t : Set α}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x / a) '' s) = s / t
theorem
Set.unionᵢ_sub
{α : Type u_1}
{ι : Sort u_2}
[inst : Sub α]
(s : ι → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => s i) - t = Set.unionᵢ fun i => s i - t
theorem
Set.unionᵢ_div
{α : Type u_1}
{ι : Sort u_2}
[inst : Div α]
(s : ι → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => s i) / t = Set.unionᵢ fun i => s i / t
theorem
Set.sub_unionᵢ
{α : Type u_1}
{ι : Sort u_2}
[inst : Sub α]
(s : Set α)
(t : ι → Set α)
:
(s - Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s - t i
theorem
Set.div_unionᵢ
{α : Type u_1}
{ι : Sort u_2}
[inst : Div α]
(s : Set α)
(t : ι → Set α)
:
(s / Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s / t i
theorem
Set.unionᵢ₂_sub
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Sub α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) - t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j - t
theorem
Set.unionᵢ₂_div
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Div α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) / t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j / t
theorem
Set.sub_unionᵢ₂
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Sub α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s - Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s - t i j
theorem
Set.div_unionᵢ₂
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Div α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s / Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s / t i j
theorem
Set.interᵢ_sub_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Sub α]
(s : ι → Set α)
(t : Set α)
:
(Set.interᵢ fun i => s i) - t ⊆ Set.interᵢ fun i => s i - t
theorem
Set.interᵢ_div_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Div α]
(s : ι → Set α)
(t : Set α)
:
(Set.interᵢ fun i => s i) / t ⊆ Set.interᵢ fun i => s i / t
theorem
Set.sub_interᵢ_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Sub α]
(s : Set α)
(t : ι → Set α)
:
(s - Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s - t i
theorem
Set.div_interᵢ_subset
{α : Type u_1}
{ι : Sort u_2}
[inst : Div α]
(s : Set α)
(t : ι → Set α)
:
(s / Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s / t i
theorem
Set.interᵢ₂_sub_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Sub α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) - t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j - t
theorem
Set.interᵢ₂_div_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Div α]
(s : (i : ι) → κ i → Set α)
(t : Set α)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) / t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j / t
theorem
Set.sub_interᵢ₂_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Sub α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s - Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s - t i j
theorem
Set.div_interᵢ₂_subset
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[inst : Div α]
(s : Set α)
(t : (i : ι) → κ i → Set α)
:
(s / Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s / t i j
def
Set.addSemigroup.proof_1
{α : Type u_1}
[inst : AddSemigroup α]
:
∀ (x x_1 x_2 : Set α),
Set.image2 (fun x x_3 => x + x_3) (Set.image2 (fun x x_3 => x + x_3) x x_1) x_2 = Set.image2 (fun x x_3 => x + x_3) x (Set.image2 (fun x x_3 => x + x_3) x_1 x_2)
Equations
- One or more equations did not get rendered due to their size.
Set α is an AddSemigroup under pointwise operations if α is.
Equations
- One or more equations did not get rendered due to their size.
def
Set.addCommSemigroup.proof_2
{α : Type u_1}
[inst : AddCommSemigroup α]
:
∀ (x x_1 : Set α), Set.image2 (fun x x_2 => x + x_2) x x_1 = Set.image2 (fun x x_2 => x + x_2) x_1 x
Equations
- (_ : Set.image2 (fun x x_1 => x + x_1) x x = Set.image2 (fun x x_1 => x + x_1) x x) = (_ : Set.image2 (fun x x_1 => x + x_1) x x = Set.image2 (fun x x_1 => x + x_1) x x)
noncomputable def
Set.addCommSemigroup
{α : Type u_1}
[inst : AddCommSemigroup α]
:
AddCommSemigroup (Set α)
Set α is an AddCommSemigroup under pointwise operations if α is.
Equations
- Set.addCommSemigroup = let src := Set.addSemigroup; AddCommSemigroup.mk (_ : ∀ (x x_1 : Set α), Set.image2 (fun x x_2 => x + x_2) x x_1 = Set.image2 (fun x x_2 => x + x_2) x_1 x)
Set α is a CommSemigroup under pointwise operations if α is.
Equations
- Set.commSemigroup = let src := Set.semigroup; CommSemigroup.mk (_ : ∀ (x x_1 : Set α), Set.image2 (fun x x_2 => x * x_2) x x_1 = Set.image2 (fun x x_2 => x * x_2) x_1 x)
Set α is an AddZeroClass under pointwise operations if α is.
Set α is a MulOneClass under pointwise operations if α is.
theorem
Set.subset_add_left
{α : Type u_1}
[inst : AddZeroClass α]
(s : Set α)
{t : Set α}
(ht : 0 ∈ t)
:
theorem
Set.subset_mul_left
{α : Type u_1}
[inst : MulOneClass α]
(s : Set α)
{t : Set α}
(ht : 1 ∈ t)
:
theorem
Set.subset_add_right
{α : Type u_1}
[inst : AddZeroClass α]
{s : Set α}
(t : Set α)
(hs : 0 ∈ s)
:
theorem
Set.subset_mul_right
{α : Type u_1}
[inst : MulOneClass α]
{s : Set α}
(t : Set α)
(hs : 1 ∈ s)
:
The singleton operation as an AddMonoidHom.
Equations
- One or more equations did not get rendered due to their size.
def
Set.singletonAddMonoidHom.proof_2
{α : Type u_1}
[inst : AddZeroClass α]
(x : α)
(y : α)
:
AddHom.toFun Set.singletonAddHom (x + y) = AddHom.toFun Set.singletonAddHom x + AddHom.toFun Set.singletonAddHom y
Equations
- One or more equations did not get rendered due to their size.
def
Set.singletonAddMonoidHom.proof_1
{α : Type u_1}
[inst : AddZeroClass α]
:
ZeroHom.toFun Set.singletonZeroHom 0 = 0
Equations
- (_ : ZeroHom.toFun Set.singletonZeroHom 0 = 0) = (_ : ZeroHom.toFun Set.singletonZeroHom 0 = 0)
The singleton operation as a MonoidHom.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Set.coe_singletonAddMonoidHom
{α : Type u_1}
[inst : AddZeroClass α]
:
↑Set.singletonAddMonoidHom = singleton
@[simp]
theorem
Set.coe_singletonMonoidHom
{α : Type u_1}
[inst : MulOneClass α]
:
↑Set.singletonMonoidHom = singleton
@[simp]
theorem
Set.singletonAddMonoidHom_apply
{α : Type u_1}
[inst : AddZeroClass α]
(a : α)
:
↑Set.singletonAddMonoidHom a = {a}
@[simp]
theorem
Set.singletonMonoidHom_apply
{α : Type u_1}
[inst : MulOneClass α]
(a : α)
:
↑Set.singletonMonoidHom a = {a}
Set α is an AddMonoid under pointwise operations if α is.
Set α is a Monoid under pointwise operations if α is.
Equations
- Set.nsmul_mem_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n
Set α is an AddCommMonoid under pointwise operations if α is.
def
Set.addCommMonoid.proof_3
{α : Type u_1}
[inst : AddCommMonoid α]
(x : Set α)
:
AddMonoid.nsmul 0 x = 0
Equations
- (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0)
def
Set.addCommMonoid.proof_4
{α : Type u_1}
[inst : AddCommMonoid α]
(n : ℕ)
(x : Set α)
:
AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
Equations
- (_ : ∀ (n : ℕ) (x : Set α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : Set α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Set α is a CommMonoid under pointwise operations if α is.
noncomputable def
Set.subtractionMonoid
{α : Type u_1}
[inst : SubtractionMonoid α]
:
SubtractionMonoid (Set α)
Set α is a subtraction monoid under pointwise operations if α is.
Equations
- One or more equations did not get rendered due to their size.
def
Set.subtractionMonoid.proof_3
{α : Type u_1}
[inst : SubtractionMonoid α]
(x : Set α)
:
AddMonoid.nsmul 0 x = 0
Equations
- (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0)
def
Set.subtractionMonoid.proof_9
{α : Type u_1}
[inst : SubtractionMonoid α]
:
∀ (n : ℕ) (a : Set α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
Equations
- (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a) = (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a)
def
Set.subtractionMonoid.proof_4
{α : Type u_1}
[inst : SubtractionMonoid α]
(n : ℕ)
(x : Set α)
:
AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
Equations
- (_ : ∀ (n : ℕ) (x : Set α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : Set α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
noncomputable def
Set.divisionMonoid
{α : Type u_1}
[inst : DivisionMonoid α]
:
DivisionMonoid (Set α)
Set α is a division monoid under pointwise operations if α is.
Equations
- One or more equations did not get rendered due to their size.
Set α is a commutative subtraction monoid under pointwise operations if α is.
Set α is a commutative division monoid under pointwise operations if α is.
noncomputable def
Set.hasDistribNeg
{α : Type u_1}
[inst : Mul α]
[inst : HasDistribNeg α]
:
HasDistribNeg (Set α)
Set α has distributive negation if α has.
Note that Set α is not a Distrib because s * t + s * u has cross terms that s * (t + u)
lacks.
Note that Set is not a MulZeroClass because 0 * ∅ ≠ 0∅ ≠ 0≠ 0.
theorem
Set.Nonempty.mul_zero
{α : Type u_1}
[inst : MulZeroClass α]
{s : Set α}
(hs : Set.Nonempty s)
:
theorem
Set.Nonempty.zero_mul
{α : Type u_1}
[inst : MulZeroClass α]
{s : Set α}
(hs : Set.Nonempty s)
:
abbrev
Set.Nonempty.zero_mem_sub.match_1
{α : Type u_1}
{s : Set α}
(motive : Set.Nonempty s → Prop)
:
(h : Set.Nonempty s) → ((a : α) → (ha : a ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive h
Equations
- Set.Nonempty.zero_mem_sub.match_1 motive h h_1 = Exists.casesOn h fun w h => h_1 w h
theorem
Set.Nonempty.zero_mem_sub
{α : Type u_1}
[inst : AddGroup α]
{s : Set α}
(h : Set.Nonempty s)
:
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Set.Nonempty.div_zero
{α : Type u_1}
[inst : GroupWithZero α]
{s : Set α}
(hs : Set.Nonempty s)
:
theorem
Set.Nonempty.zero_div
{α : Type u_1}
[inst : GroupWithZero α]
{s : Set α}
(hs : Set.Nonempty s)
: