Self-inverse finsets

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

See also Algebra/Group/Pointwise/Set/SelfInv.lean for the set version.

@[simp]

theorem Finset.isSelfInv_coe_iff {α : Type u_1} [DecidableEq α] [InvolutiveInv α] {s : Finset α} : IsSelfInv ↑s ↔ IsSelfInv s

@[simp]

theorem Finset.isSelfNeg_coe_iff {α : Type u_1} [DecidableEq α] [InvolutiveNeg α] {s : Finset α} : IsSelfNeg ↑s ↔ IsSelfNeg s

theorem Finset.IsSelfInv.of_coe_finset {α : Type u_1} [DecidableEq α] [InvolutiveInv α] {s : Finset α} : IsSelfInv ↑s → IsSelfInv s

Alias of the forward direction of Finset.isSelfInv_coe_iff.

theorem Finset.IsSelfInv.coe_finset {α : Type u_1} [DecidableEq α] [InvolutiveInv α] {s : Finset α} : IsSelfInv s → IsSelfInv ↑s

Alias of the reverse direction of Finset.isSelfInv_coe_iff.

theorem Finset.IsSelfNeg.coe_finset {α : Type u_1} [DecidableEq α] [InvolutiveNeg α] {s : Finset α} : IsSelfNeg s → IsSelfNeg ↑s

Alias of the reverse direction of Finset.isSelfNeg_coe_iff.

theorem Finset.IsSelfNeg.of_coe_finset {α : Type u_1} [DecidableEq α] [InvolutiveNeg α] {s : Finset α} : IsSelfNeg ↑s → IsSelfNeg s

Alias of the forward direction of Finset.isSelfNeg_coe_iff.

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

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