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]
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]
@[simp]
theorem
set.nonempty_star
{α : Type u_1}
[has_involutive_star α]
{s : set α} :
(has_star.star s).nonempty ↔ s.nonempty
@[simp]
theorem
set.mem_star
{α : Type u_1}
{s : set α}
{a : α}
[has_star α] :
a ∈ has_star.star s ↔ has_star.star a ∈ s
theorem
set.star_mem_star
{α : Type u_1}
{s : set α}
{a : α}
[has_involutive_star α] :
has_star.star a ∈ has_star.star s ↔ a ∈ s
@[simp]
@[simp]
@[simp]
theorem
set.inter_star
{α : Type u_1}
{s t : set α}
[has_star α] :
has_star.star (s ∩ t) = has_star.star s ∩ has_star.star t
@[simp]
theorem
set.union_star
{α : Type u_1}
{s t : set α}
[has_star α] :
has_star.star (s ∪ t) = has_star.star s ∪ has_star.star t
@[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 α] :
has_star.star sᶜ = (has_star.star s)ᶜ
@[protected, simp, instance]
Equations
@[simp]
theorem
set.star_subset_star
{α : Type u_1}
[has_involutive_star α]
{s t : set α} :
has_star.star s ⊆ has_star.star t ↔ s ⊆ t
theorem
set.star_subset
{α : Type u_1}
[has_involutive_star α]
{s t : set α} :
has_star.star s ⊆ t ↔ s ⊆ has_star.star t
theorem
set.finite.star
{α : Type u_1}
[has_involutive_star α]
{s : set α}
(hs : s.finite) :
(has_star.star s).finite
theorem
set.star_singleton
{β : Type u_1}
[has_involutive_star β]
(x : β) :
has_star.star {x} = {has_star.star x}
@[protected]
theorem
set.star_mul
{α : Type u_1}
[monoid α]
[star_semigroup α]
(s t : set α) :
has_star.star (s * t) = has_star.star t * has_star.star s
@[protected]
theorem
set.star_add
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(s t : set α) :
has_star.star (s + t) = has_star.star s + has_star.star t
@[protected, simp, instance]
def
set.has_trivial_star
{α : Type u_1}
[has_star α]
[has_trivial_star α] :
has_trivial_star (set α)
@[protected]
theorem
set.star_inv
{α : Type u_1}
[group α]
[star_semigroup α]
(s : set α) :
has_star.star s⁻¹ = (has_star.star s)⁻¹
@[protected]
theorem
set.star_inv'
{α : Type u_1}
[division_ring α]
[star_ring α]
(s : set α) :
has_star.star s⁻¹ = (has_star.star s)⁻¹