Pointwise operations of finsets #
This file defines pointwise algebraic operations on finsets.
Main declarations #
For finsets s
and t
:
0
(Finset.zero
): The singleton{0}
.1
(Finset.one
): The singleton{1}
.-s
(Finset.neg
): Negation, finset of all-x
wherex ∈ s
.s⁻¹
(Finset.inv
): Inversion, finset of allx⁻¹
wherex ∈ s
.s + t
(Finset.add
): Addition, finset of allx + y
wherex ∈ s
andy ∈ t
.s * t
(Finset.mul
): Multiplication, finset of allx * y
wherex ∈ s
andy ∈ t
.s - t
(Finset.sub
): Subtraction, finset of allx - y
wherex ∈ s
andy ∈ t
.s / t
(Finset.div
): Division, finset of allx / y
wherex ∈ s
andy ∈ t
.s +ᵥ t
(Finset.vadd
): Scalar addition, finset of allx +ᵥ y
wherex ∈ s
andy ∈ t
.s • t
(Finset.smul
): Scalar multiplication, finset of allx • y
wherex ∈ s
andy ∈ t
.s -ᵥ t
(Finset.vsub
): Scalar subtraction, finset of allx -ᵥ y
wherex ∈ s
andy ∈ t
.a • s
(Finset.smulFinset
): Scaling, finset of alla • x
wherex ∈ s
.a +ᵥ s
(Finset.vaddFinset
): Translation, finset of alla +ᵥ x
wherex ∈ s
.
For α
a semigroup/monoid, Finset α
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].
Implementation notes #
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 of simp
.
Tags #
finset multiplication, finset addition, pointwise addition, pointwise multiplication, pointwise subtraction
0
/1
as finsets #
Lift a ZeroHom
to Finset
via image
Equations
- Finset.imageZeroHom f = { toFun := Finset.image ⇑f, map_zero' := ⋯ }
Instances For
Lift a OneHom
to Finset
via image
.
Equations
- Finset.imageOneHom f = { toFun := Finset.image ⇑f, map_one' := ⋯ }
Instances For
Finset negation/inversion #
The pointwise negation of finset -s
is defined as {-x | x ∈ s}
in locale Pointwise
.
Equations
- Finset.neg = { neg := Finset.image Neg.neg }
Instances For
The pointwise inversion of finset s⁻¹
is defined as {x⁻¹ | x ∈ s}
in locale Pointwise
.
Equations
- Finset.inv = { inv := Finset.image Inv.inv }
Instances For
Alias of the forward direction of Finset.inv_nonempty_iff
.
Alias of the reverse direction of Finset.inv_nonempty_iff
.
Finset addition/multiplication #
The pointwise addition of finsets s + t
is defined as {x + y | x ∈ s, y ∈ t}
in
locale Pointwise
.
Equations
- Finset.add = { add := Finset.image₂ fun (x1 x2 : α) => x1 + x2 }
Instances For
The pointwise multiplication of finsets s * t
and t
is defined as {x * y | x ∈ s, y ∈ t}
in locale Pointwise
.
Equations
- Finset.mul = { mul := Finset.image₂ fun (x1 x2 : α) => x1 * x2 }
Instances For
If a finset u
is contained in the sum of two sets s + t
, we can find two finsets
s'
, t'
such that s' ⊆ s
, t' ⊆ t
and u ⊆ s' + t'
.
If a finset u
is contained in the product of two sets s * t
, we can find two finsets s'
,
t'
such that s' ⊆ s
, t' ⊆ t
and u ⊆ s' * t'
.
Lift an AddHom
to Finset
via image
Equations
- Finset.imageAddHom f = { toFun := Finset.image ⇑f, map_add' := ⋯ }
Instances For
Lift a MulHom
to Finset
via image
.
Equations
- Finset.imageMulHom f = { toFun := Finset.image ⇑f, map_mul' := ⋯ }
Instances For
Finset subtraction/division #
The pointwise subtraction of finsets s - t
is defined as {x - y | x ∈ s, y ∈ t}
in locale Pointwise
.
Equations
- Finset.sub = { sub := Finset.image₂ fun (x1 x2 : α) => x1 - x2 }
Instances For
The pointwise division of finsets s / t
is defined as {x / y | x ∈ s, y ∈ t}
in locale
Pointwise
.
Equations
- Finset.div = { div := Finset.image₂ fun (x1 x2 : α) => x1 / x2 }
Instances For
If a finset u
is contained in the sum of two sets s - t
, we can find two finsets
s'
, t'
such that s' ⊆ s
, t' ⊆ t
and u ⊆ s' - t'
.
If a finset u
is contained in the product of two sets s / t
, we can find two finsets s'
,
t'
such that s' ⊆ s
, t' ⊆ t
and u ⊆ s' / t'
.
Instances #
Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
Finset
. See note [pointwise nat action].
Instances For
Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a Finset
. See note [pointwise nat action].
Instances For
Finset α
is an AddSemigroup
under pointwise operations if α
is.
Equations
- Finset.addSemigroup = Function.Injective.addSemigroup Finset.toSet ⋯ ⋯
Instances For
Finset α
is a Semigroup
under pointwise operations if α
is.
Equations
- Finset.semigroup = Function.Injective.semigroup Finset.toSet ⋯ ⋯
Instances For
Finset α
is an AddCommSemigroup
under pointwise operations if α
is.
Equations
- Finset.addCommSemigroup = Function.Injective.addCommSemigroup Finset.toSet ⋯ ⋯
Instances For
Finset α
is a CommSemigroup
under pointwise operations if α
is.
Equations
- Finset.commSemigroup = Function.Injective.commSemigroup Finset.toSet ⋯ ⋯
Instances For
Finset α
is an AddZeroClass
under pointwise operations if α
is.
Equations
- Finset.addZeroClass = Function.Injective.addZeroClass Finset.toSet ⋯ ⋯ ⋯
Instances For
Finset α
is a MulOneClass
under pointwise operations if α
is.
Equations
- Finset.mulOneClass = Function.Injective.mulOneClass Finset.toSet ⋯ ⋯ ⋯
Instances For
The singleton operation as an AddMonoidHom
.
Equations
- Finset.singletonAddMonoidHom = { toFun := Finset.singletonAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The coercion from Finset
to set
as an AddMonoidHom
.
Equations
- Finset.coeAddMonoidHom = { toFun := CoeTC.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The coercion from Finset
to Set
as a MonoidHom
.
Equations
- Finset.coeMonoidHom = { toFun := CoeTC.coe, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Lift an add_monoid_hom
to Finset
via image
Equations
- Finset.imageAddMonoidHom f = { toFun := (Finset.imageAddHom f).toFun, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Lift a MonoidHom
to Finset
via image
.
Equations
- Finset.imageMonoidHom f = { toFun := (Finset.imageMulHom f).toFun, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Finset α
is an AddMonoid
under pointwise operations if α
is.
Equations
- Finset.addMonoid = Function.Injective.addMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is a Monoid
under pointwise operations if α
is.
Equations
- Finset.monoid = Function.Injective.monoid Finset.toSet ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is an AddCommMonoid
under pointwise operations if α
is.
Equations
- Finset.addCommMonoid = Function.Injective.addCommMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is a CommMonoid
under pointwise operations if α
is.
Equations
- Finset.commMonoid = Function.Injective.commMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is a subtraction monoid under pointwise operations if α
is.
Equations
- Finset.subtractionMonoid = Function.Injective.subtractionMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is a division monoid under pointwise operations if α
is.
Equations
- Finset.divisionMonoid = Function.Injective.divisionMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is a commutative subtraction monoid under pointwise operations if α
is.
Equations
- Finset.subtractionCommMonoid = Function.Injective.subtractionCommMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
is a commutative division monoid under pointwise operations if α
is.
Equations
- Finset.divisionCommMonoid = Function.Injective.divisionCommMonoid Finset.toSet ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Finset α
has distributive negation if α
has.
Equations
- Finset.distribNeg = Function.Injective.hasDistribNeg Finset.toSet ⋯ ⋯ ⋯
Instances For
Note that Finset α
is not a Distrib
because s * t + s * u
has cross terms that s * (t + u)
lacks.
-- {10, 16, 18, 20, 8, 9}
#eval {1, 2} * ({3, 4} + {5, 6} : Finset ℕ)
-- {10, 11, 12, 13, 14, 15, 16, 18, 20, 8, 9}
#eval ({1, 2} : Finset ℕ) * {3, 4} + {1, 2} * {5, 6}
Note that Finset
is not a MulZeroClass
because 0 * ∅ ≠ 0
.
Scalar addition/multiplication of finsets #
The pointwise sum of two finsets s
and t
: s +ᵥ t = {x +ᵥ y | x ∈ s, y ∈ t}
.
Equations
- Finset.vadd = { vadd := Finset.image₂ fun (x1 : α) (x2 : β) => x1 +ᵥ x2 }
Instances For
The pointwise product of two finsets s
and t
: s • t = {x • y | x ∈ s, y ∈ t}
.
Equations
- Finset.smul = { smul := Finset.image₂ fun (x1 : α) (x2 : β) => x1 • x2 }