Self-inverse sets

This file specialises IsSelfInv to sets equipped with the pointwise inversion.

See also Mathlib/Algebra/Group/Pointwise/Finset/SelfInv.lean for the finset version.

theorem Set.isSelfInv_iff_forall_inv_mem_iff {α : Type u_1} [Inv α] {s : Set α} : IsSelfInv s ↔ ∀ (x : α), x⁻¹ ∈ s ↔ x ∈ s

theorem Set.isSelfNeg_iff_forall_neg_mem_iff {α : Type u_1} [Neg α] {s : Set α} : IsSelfNeg s ↔ ∀ (x : α), -x ∈ s ↔ x ∈ s

@[simp]

theorem Set.IsSelfInv.empty {α : Type u_1} [Inv α] : IsSelfInv ∅

@[simp]

theorem Set.IsSelfNeg.empty {α : Type u_1} [Neg α] : IsSelfNeg ∅

@[simp]

theorem Set.IsSelfInv.univ {α : Type u_1} [Inv α] : IsSelfInv univ

@[simp]

theorem Set.IsSelfNeg.univ {α : Type u_1} [Neg α] : IsSelfNeg univ

theorem Set.IsSelfInv.inter {α : Type u_1} [Inv α] {s t : Set α} (hs : IsSelfInv s) (ht : IsSelfInv t) : IsSelfInv (s ∩ t)

theorem Set.IsSelfNeg.inter {α : Type u_1} [Neg α] {s t : Set α} (hs : IsSelfNeg s) (ht : IsSelfNeg t) : IsSelfNeg (s ∩ t)

theorem Set.IsSelfInv.union {α : Type u_1} [Inv α] {s t : Set α} (hs : IsSelfInv s) (ht : IsSelfInv t) : IsSelfInv (s ∪ t)

theorem Set.IsSelfNeg.union {α : Type u_1} [Neg α] {s t : Set α} (hs : IsSelfNeg s) (ht : IsSelfNeg t) : IsSelfNeg (s ∪ t)

theorem Set.IsSelfInv.iUnion {α : Type u_1} [Inv α] {ι : Sort u_3} {s : ι → Set α} (h : ∀ (i : ι), IsSelfInv (s i)) : IsSelfInv (⋃ (i : ι), s i)

theorem Set.IsSelfNeg.iUnion {α : Type u_1} [Neg α] {ι : Sort u_3} {s : ι → Set α} (h : ∀ (i : ι), IsSelfNeg (s i)) : IsSelfNeg (⋃ (i : ι), s i)

theorem Set.IsSelfInv.iInter {α : Type u_1} [Inv α] {ι : Sort u_3} {s : ι → Set α} (h : ∀ (i : ι), IsSelfInv (s i)) : IsSelfInv (⋂ (i : ι), s i)

theorem Set.IsSelfNeg.iInter {α : Type u_1} [Neg α] {ι : Sort u_3} {s : ι → Set α} (h : ∀ (i : ι), IsSelfNeg (s i)) : IsSelfNeg (⋂ (i : ι), s i)

theorem Set.IsSelfInv.sUnion {α : Type u_1} [Inv α] {S : Set (Set α)} (h : ∀ s ∈ S, IsSelfInv s) : IsSelfInv (⋃₀ S)

theorem Set.IsSelfNeg.sUnion {α : Type u_1} [Neg α] {S : Set (Set α)} (h : ∀ s ∈ S, IsSelfNeg s) : IsSelfNeg (⋃₀ S)

theorem Set.IsSelfInv.sInter {α : Type u_1} [Inv α] {S : Set (Set α)} (h : ∀ s ∈ S, IsSelfInv s) : IsSelfInv (⋂₀ S)

theorem Set.IsSelfNeg.sInter {α : Type u_1} [Neg α] {S : Set (Set α)} (h : ∀ s ∈ S, IsSelfNeg s) : IsSelfNeg (⋂₀ S)

theorem Set.IsSelfInv.prod {α : Type u_1} {β : Type u_2} [Inv α] [Inv β] {s : Set α} {t : Set β} (hs : IsSelfInv s) (ht : IsSelfInv t) : IsSelfInv (s ×ˢ t)

theorem Set.IsSelfNeg.prod {α : Type u_1} {β : Type u_2} [Neg α] [Neg β] {s : Set α} {t : Set β} (hs : IsSelfNeg s) (ht : IsSelfNeg t) : IsSelfNeg (s ×ˢ t)

@[simp]

theorem Set.isSelfInv_compl_iff {α : Type u_1} [Inv α] {s : Set α} : IsSelfInv sᶜ ↔ IsSelfInv s

@[simp]

theorem Set.isSelfNeg_compl_iff {α : Type u_1} [Neg α] {s : Set α} : IsSelfNeg sᶜ ↔ IsSelfNeg s

theorem Set.IsSelfInv.of_compl {α : Type u_1} [Inv α] {s : Set α} : IsSelfInv sᶜ → IsSelfInv s

Alias of the forward direction of Set.isSelfInv_compl_iff.

theorem Set.IsSelfInv.compl {α : Type u_1} [Inv α] {s : Set α} : IsSelfInv s → IsSelfInv sᶜ

Alias of the reverse direction of Set.isSelfInv_compl_iff.

theorem Set.IsSelfNeg.compl {α : Type u_1} [Neg α] {s : Set α} : IsSelfNeg s → IsSelfNeg sᶜ

Alias of the reverse direction of Set.isSelfNeg_compl_iff.

theorem Set.IsSelfNeg.of_compl {α : Type u_1} [Neg α] {s : Set α} : IsSelfNeg sᶜ → IsSelfNeg s

Alias of the forward direction of Set.isSelfNeg_compl_iff.

@[simp]

theorem Set.isSelfInv_singleton_iff {α : Type u_1} [InvolutiveInv α] {a : α} : IsSelfInv {a} ↔ IsSelfInv a

@[simp]

theorem Set.isSelfNeg_singleton_iff {α : Type u_1} [InvolutiveNeg α] {a : α} : IsSelfNeg {a} ↔ IsSelfNeg a

theorem Set.isSelfInv_iff_subset_inv {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s ↔ s ⊆ s⁻¹

theorem Set.isSelfNeg_iff_subset_neg {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg s ↔ s ⊆ -s

theorem Set.IsSelfInv.subset_inv {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s → s ⊆ s⁻¹

Alias of the forward direction of Set.isSelfInv_iff_subset_inv.

theorem Set.IsSelfInv.of_subset_inv {α : Type u_1} [InvolutiveInv α] {s : Set α} : s ⊆ s⁻¹ → IsSelfInv s

Alias of the reverse direction of Set.isSelfInv_iff_subset_inv.

theorem Set.IsSelfNeg.subset_neg {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg s → s ⊆ -s

Alias of the forward direction of Set.isSelfNeg_iff_subset_neg.

theorem Set.IsSelfNeg.of_subset_neg {α : Type u_1} [InvolutiveNeg α] {s : Set α} : s ⊆ -s → IsSelfNeg s

Alias of the reverse direction of Set.isSelfNeg_iff_subset_neg.

theorem Set.isSelfInv_iff_inv_subset {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s ↔ s⁻¹ ⊆ s

theorem Set.isSelfNeg_iff_neg_subset {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg s ↔ -s ⊆ s

theorem Set.IsSelfInv.of_inv_subset {α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹ ⊆ s → IsSelfInv s

Alias of the reverse direction of Set.isSelfInv_iff_inv_subset.

theorem Set.IsSelfInv.inv_subset {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s → s⁻¹ ⊆ s

Alias of the forward direction of Set.isSelfInv_iff_inv_subset.

theorem Set.IsSelfNeg.neg_subset {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg s → -s ⊆ s

Alias of the forward direction of Set.isSelfNeg_iff_neg_subset.

theorem Set.IsSelfNeg.of_neg_subset {α : Type u_1} [InvolutiveNeg α] {s : Set α} : -s ⊆ s → IsSelfNeg s

Alias of the reverse direction of Set.isSelfNeg_iff_neg_subset.

theorem Set.isSelfInv_iff_forall_inv_mem {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s ↔ ∀ ⦃x : α⦄, x ∈ s → x⁻¹ ∈ s

theorem Set.isSelfNeg_iff_forall_neg_mem {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg s ↔ ∀ ⦃x : α⦄, x ∈ s → -x ∈ s

theorem Set.IsSelfInv.inv_mem {α : Type u_1} [InvolutiveInv α] {s : Set α} (h : IsSelfInv s) {x : α} (hx : x ∈ s) : x⁻¹ ∈ s

theorem Set.IsSelfNeg.neg_mem {α : Type u_1} [InvolutiveNeg α] {s : Set α} (h : IsSelfNeg s) {x : α} (hx : x ∈ s) : -x ∈ s

theorem Set.IsSelfInv.diff {α : Type u_1} [InvolutiveInv α] {s t : Set α} (hs : IsSelfInv s) (ht : IsSelfInv t) : IsSelfInv (s \ t)

theorem Set.IsSelfNeg.diff {α : Type u_1} [InvolutiveNeg α] {s t : Set α} (hs : IsSelfNeg s) (ht : IsSelfNeg t) : IsSelfNeg (s \ t)

theorem Set.isSelfInv_inter_inv {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv (s ∩ s⁻¹)

theorem Set.isSelfNeg_inter_neg {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg (s ∩ -s)

theorem Set.isSelfInv_union_inv {α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv (s ∪ s⁻¹)

theorem Set.isSelfNeg_union_neg {α : Type u_1} [InvolutiveNeg α] {s : Set α} : IsSelfNeg (s ∪ -s)

theorem Set.IsSelfInv.image {α : Type u_1} {β : Type u_2} [Group α] [DivisionMonoid β] {F : Type u_3} [FunLike F α β] [MonoidHomClass F α β] {s : Set α} (f : F) (hs : IsSelfInv s) : IsSelfInv (⇑f '' s)

theorem Set.IsSelfNeg.image {α : Type u_1} {β : Type u_2} [AddGroup α] [SubtractionMonoid β] {F : Type u_3} [FunLike F α β] [AddMonoidHomClass F α β] {s : Set α} (f : F) (hs : IsSelfNeg s) : IsSelfNeg (⇑f '' s)