mathlib3 documentation

data.set.semiring

Sets as a semiring under union #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines set_semiring α, an alias of set α, which we endow with ∪ as addition and pointwise * as multiplication. If α is a (commutative) monoid, set_semiring α is a (commutative) semiring.

source
@[protected, instance]
def set_semiring.order_bot (α : Type u_1) :
order_bot (set_semiring α)
source
@[protected, instance]
def set_semiring.inhabited (α : Type u_1) :
inhabited (set_semiring α)
source
@[protected, instance]
def set_semiring.partial_order (α : Type u_1) :
partial_order (set_semiring α)
source
def set_semiring (α : Type u_1) :
Type u_1

An alias for set α, which has a semiring structure given by ∪ as "addition" and pointwise multiplication * as "multiplication".

Equations
Instances for set_semiring
source
@[protected]
def set.up {α : Type u_1} :
set α ≃ set_semiring α

The identity function set α → set_semiring α.

Equations
source
@[protected]
def set_semiring.down {α : Type u_1} :
set_semiring α ≃ set α

The identity function set_semiring α → set α.

Equations
source
@[protected, simp]
theorem set_semiring.down_up {α : Type u_1} (s : set α) :
⇑set_semiring.down (⇑set.up s) = s
source
@[protected, simp]
theorem set_semiring.up_down {α : Type u_1} (s : set_semiring α) :
⇑set.up (⇑set_semiring.down s) = s
source
theorem set_semiring.up_le_up {α : Type u_1} {s t : set α} :
⇑set.up s ≤ ⇑set.up t ↔ s ⊆ t
source
theorem set_semiring.up_lt_up {α : Type u_1} {s t : set α} :
⇑set.up s < ⇑set.up t ↔ s ⊂ t
source
@[simp]
theorem set_semiring.down_subset_down {α : Type u_1} {s t : set_semiring α} :
⇑set_semiring.down s ⊆ ⇑set_semiring.down t ↔ s ≤ t
source
@[simp]
theorem set_semiring.down_ssubset_down {α : Type u_1} {s t : set_semiring α} :
⇑set_semiring.down s ⊂ ⇑set_semiring.down t ↔ s < t
source
@[protected, instance]
def set_semiring.add_comm_monoid {α : Type u_1} :
add_comm_monoid (set_semiring α)
Equations
source
theorem set_semiring.zero_def {α : Type u_1} :
0 = ⇑set.up ∅
source
@[simp]
theorem set_semiring.down_zero {α : Type u_1} :
⇑set_semiring.down 0 = ∅
source
@[simp]
theorem set.up_empty {α : Type u_1} :
⇑set.up ∅ = 0
source
theorem set_semiring.add_def {α : Type u_1} (s t : set_semiring α) :
s + t = ⇑set.up (⇑set_semiring.down s ∪ ⇑set_semiring.down t)
source
@[simp]
theorem set_semiring.down_add {α : Type u_1} (s t : set_semiring α) :
⇑set_semiring.down (s + t) = ⇑set_semiring.down s ∪ ⇑set_semiring.down t
source
@[simp]
theorem set.up_union {α : Type u_1} (s t : set α) :
⇑set.up (s ∪ t) = ⇑set.up s + ⇑set.up t
source
@[protected, instance]
def set_semiring.covariant_class_add {α : Type u_1} :
covariant_class (set_semiring α) (set_semiring α) has_add.add has_le.le
source
@[protected, instance]
def set_semiring.non_unital_non_assoc_semiring {α : Type u_1} [has_mul α] :
non_unital_non_assoc_semiring (set_semiring α)
Equations
source
theorem set_semiring.mul_def {α : Type u_1} [has_mul α] (s t : set_semiring α) :
s * t = ⇑set.up (⇑set_semiring.down s * ⇑set_semiring.down t)
source
@[simp]
theorem set_semiring.down_mul {α : Type u_1} [has_mul α] (s t : set_semiring α) :
⇑set_semiring.down (s * t) = ⇑set_semiring.down s * ⇑set_semiring.down t
source
@[simp]
theorem set.up_mul {α : Type u_1} [has_mul α] (s t : set α) :
⇑set.up (s * t) = ⇑set.up s * ⇑set.up t
source
@[protected, instance]
def set_semiring.no_zero_divisors {α : Type u_1} [has_mul α] :
no_zero_divisors (set_semiring α)
source
@[protected, instance]
def set_semiring.covariant_class_mul_left {α : Type u_1} [has_mul α] :
covariant_class (set_semiring α) (set_semiring α) has_mul.mul has_le.le
source
@[protected, instance]
def set_semiring.covariant_class_mul_right {α : Type u_1} [has_mul α] :
covariant_class (set_semiring α) (set_semiring α) (function.swap has_mul.mul) has_le.le
source
@[protected, instance]
def set_semiring.has_one {α : Type u_1} [has_one α] :
has_one (set_semiring α)
Equations
source
theorem set_semiring.one_def {α : Type u_1} [has_one α] :
1 = ⇑set.up 1
source
@[simp]
theorem set_semiring.down_one {α : Type u_1} [has_one α] :
⇑set_semiring.down 1 = 1
source
@[simp]
theorem set.up_one {α : Type u_1} [has_one α] :
⇑set.up 1 = 1
source
@[protected, instance]
def set_semiring.non_assoc_semiring {α : Type u_1} [mul_one_class α] :
non_assoc_semiring (set_semiring α)
Equations
source
@[protected, instance]
def set_semiring.non_unital_semiring {α : Type u_1} [semigroup α] :
non_unital_semiring (set_semiring α)
Equations
source
@[protected, instance]
def set_semiring.idem_semiring {α : Type u_1} [monoid α] :
idem_semiring (set_semiring α)
Equations
source
@[protected, instance]
def set_semiring.non_unital_comm_semiring {α : Type u_1} [comm_semigroup α] :
non_unital_comm_semiring (set_semiring α)
Equations
source
@[protected, instance]
def set_semiring.idem_comm_semiring {α : Type u_1} [comm_monoid α] :
idem_comm_semiring (set_semiring α)
Equations
source
@[protected, instance]
def set_semiring.canonically_ordered_comm_semiring {α : Type u_1} [comm_monoid α] :
canonically_ordered_comm_semiring (set_semiring α)
Equations
source
def set_semiring.image_hom {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) :
set_semiring α →+* set_semiring β

The image of a set under a multiplicative homomorphism is a ring homomorphism with respect to the pointwise operations on sets.

Equations
source
theorem set_semiring.image_hom_def {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (s : set_semiring α) :
⇑(set_semiring.image_hom f) s = ⇑set.up (⇑f '' ⇑set_semiring.down s)
source
@[simp]
theorem set_semiring.down_image_hom {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (s : set_semiring α) :
⇑set_semiring.down (⇑(set_semiring.image_hom f) s) = ⇑f '' ⇑set_semiring.down s
source
@[simp]
theorem set.up_image {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (s : set α) :
⇑set.up (⇑f '' s) = ⇑(set_semiring.image_hom f) (⇑set.up s)