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
(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_semiring α]
[star_ring α]
(s : set α) :
has_star.star s⁻¹ = (has_star.star s)⁻¹