Self-inverse sets

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of isSelfInv_compl_iff.

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

Alias of the forward direction of isSelfInv_compl_iff.

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

Alias of the forward direction of isSelfNeg_compl_iff.

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

Alias of the reverse direction of isSelfNeg_compl_iff.

@[simp]

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

@[simp]

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

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

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

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

Alias of the reverse direction of isSelfInv_iff_subset_inv.

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

Alias of the forward direction of isSelfInv_iff_subset_inv.

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

Alias of the forward direction of isSelfNeg_iff_subset_neg.

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

Alias of the reverse direction of isSelfNeg_iff_subset_neg.

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

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

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

Alias of the forward direction of isSelfInv_iff_inv_subset.

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

Alias of the reverse direction of isSelfInv_iff_inv_subset.

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

Alias of the reverse direction of isSelfNeg_iff_neg_subset.

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

Alias of the forward direction of isSelfNeg_iff_neg_subset.

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

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

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

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

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

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