mathlib3 documentation

algebra.star.pointwise

Pointwise star operation on sets #

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

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

@[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]
@[simp]
theorem set.nonempty_star {α : Type u_1} [has_involutive_star α] {s : set α} :
theorem set.nonempty.star {α : Type u_1} [has_involutive_star α] {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 : α} [has_involutive_star α] :
@[simp]
theorem set.star_preimage {α : Type u_1} {s : set α} [has_star α] :
@[simp]
theorem set.image_star {α : Type u_1} {s : set α} [has_involutive_star α] :
@[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 α] :
@[simp]
theorem set.star_subset_star {α : Type u_1} [has_involutive_star α] {s t : set α} :
theorem set.star_subset {α : Type u_1} [has_involutive_star α] {s t : set α} :
theorem set.finite.star {α : Type u_1} [has_involutive_star α] {s : set α} (hs : s.finite) :
theorem set.star_singleton {β : Type u_1} [has_involutive_star β] (x : β) :
@[protected]
theorem set.star_mul {α : Type u_1} [monoid α] [star_semigroup α] (s t : set α) :
@[protected]
theorem set.star_add {α : Type u_1} [add_monoid α] [star_add_monoid α] (s t : set α) :
@[protected, simp, instance]
@[protected]
theorem set.star_inv {α : Type u_1} [group α] [star_semigroup α] (s : set α) :
@[protected]
theorem set.star_inv' {α : Type u_1} [division_semiring α] [star_ring α] (s : set α) :