# mathlibdocumentation

algebra.star.pointwise

# Pointwise star operation on sets #

This file defines the star operation pointwise on sets and provides the basic API. Besides basic facts about about how the star operation acts on sets (e.g., (s ∩ t)⋆ = s⋆ ∩ t⋆), if s t : set α, then under suitable assumption on α, it is shown

• (s + t)⋆ = s⋆ + t⋆
• (s * t)⋆ = t⋆ + s⋆
• (s⁻¹)⋆ = (s⋆)⁻¹
@[protected]
def set.has_star {α : Type u_1} [has_star α] :

The set (star s : set α) is defined as {x | star x ∈ s} in locale pointwise. In the usual case where star is involutive, it is equal to {star s | x ∈ s}, see set.image_star.

Equations
@[simp]
theorem set.star_empty {α : Type u_1} [has_star α] :
@[simp]
theorem set.star_univ {α : Type u_1} [has_star α] :
@[simp]
theorem set.nonempty_star {α : Type u_1} {s : set α} :
theorem set.nonempty.star {α : Type u_1} {s : set α} (h : s.nonempty) :
@[simp]
theorem set.mem_star {α : Type u_1} {s : set α} {a : α} [has_star α] :
theorem set.star_mem_star {α : Type u_1} {s : set α} {a : α}  :
a s
@[simp]
theorem set.star_preimage {α : Type u_1} {s : set α} [has_star α] :
@[simp]
theorem set.image_star {α : Type u_1} {s : set α}  :
@[simp]
theorem set.inter_star {α : Type u_1} {s t : set α} [has_star α] :
@[simp]
theorem set.union_star {α : Type u_1} {s t : set α} [has_star α] :
@[simp]
theorem set.Inter_star {α : Type u_1} {ι : Sort u_2} [has_star α] (s : ι → set α) :
has_star.star (⋂ (i : ι), s i) = ⋂ (i : ι), has_star.star (s i)
@[simp]
theorem set.Union_star {α : Type u_1} {ι : Sort u_2} [has_star α] (s : ι → set α) :
has_star.star (⋃ (i : ι), s i) = ⋃ (i : ι), has_star.star (s i)
@[simp]
theorem set.compl_star {α : Type u_1} {s : set α} [has_star α] :
@[protected, simp, instance]
def set.has_involutive_star {α : Type u_1}  :
Equations
@[simp]
theorem set.star_subset_star {α : Type u_1} {s t : set α} :
s t
theorem set.star_subset {α : Type u_1} {s t : set α} :
theorem set.finite.star {α : Type u_1} {s : set α} (hs : s.finite) :
theorem set.star_singleton {β : Type u_1} (x : β) :
=
@[protected]
theorem set.star_mul {α : Type u_1} [monoid α] (s t : set α) :
@[protected]
theorem set.star_add {α : Type u_1} [add_monoid α] (s t : set α) :
@[protected, simp, instance]
def set.has_trivial_star {α : Type u_1} [has_star α]  :
@[protected]
theorem set.star_inv {α : Type u_1} [group α] (s : set α) :
@[protected]
theorem set.star_inv' {α : Type u_1} [star_ring α] (s : set α) :