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 * y
wherex ∈ s∈ s
andy ∈ t∈ t
.s + t
: Addition, set of allx + y
wherex ∈ s∈ s
andy ∈ t∈ t
.s⁻¹⁻¹
: Inversion, set of allx⁻¹⁻¹
wherex ∈ s∈ s
.-s
: Negation, set of all-x
wherex ∈ s∈ s
.s / t
: Division, set of allx / y
wherex ∈ s∈ s
andy ∈ t∈ t
.s - t
: Subtraction, set of allx - y
wherex ∈ s∈ s
andy ∈ 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 #
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 }
Set addition/multiplication #
Set subtraction/division #
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.
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)
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.
The singleton operation as an AddMonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
Equations
- (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0)
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.
Set α
is a subtraction monoid under pointwise operations if α
is.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : Set α), AddMonoid.nsmul 0 x = 0)
Equations
- (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a) = (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a)
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 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.
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
.
Equations
- Set.Nonempty.zero_mem_sub.match_1 motive h h_1 = Exists.casesOn h fun w h => h_1 w h