The symmetric square

This file defines the symmetric square, which is α × α modulo swapping. This is also known as the type of unordered pairs.

More generally, the symmetric square is the second symmetric power (see Data.Sym.Basic). The equivalence is Sym2.equivSym.

From the point of view that an unordered pair is equivalent to a multiset of cardinality two (see Sym2.equivMultiset), there is a Mem instance Sym2.Mem, which is a Prop-valued membership test. Given h : a ∈ z for z : Sym2 α, then Mem.other h is the other element of the pair, defined using Classical.choice. If α has decidable equality, then h.other' computably gives the other element.

The universal property of Sym2 is provided as Sym2.lift, which states that functions from Sym2 α are equivalent to symmetric two-argument functions from α.

Recall that an undirected graph (allowing self loops, but no multiple edges) is equivalent to a symmetric relation on the vertex type α. Given a symmetric relation on α, the corresponding edge set is constructed by Sym2.fromRel which is a special case of Sym2.lift.

Notation

The element Sym2.mk (a, b) can be written as s(a, b) for short.

Tags

symmetric square, unordered pairs, symmetric powers

inductive Sym2.Rel (α : Type u) : α × α → α × α → Prop

This is the relation capturing the notion of pairs equivalent up to permutations.

• refl {α : Type u} (x y : α) : Rel α (x, y) (x, y)
• swap {α : Type u} (x y : α) : Rel α (x, y) (y, x)

theorem Sym2.Rel.symm {α : Type u_1} {x y : α × α} : Rel α x y → Rel α y x

theorem Sym2.Rel.trans {α : Type u_1} {x y z : α × α} (a : Rel α x y) (b : Rel α y z) : Rel α x z

theorem Sym2.Rel.is_equivalence {α : Type u_1} : Equivalence (Rel α)

@[implicit_reducible]

def Sym2.Rel.setoid (α : Type u) : Setoid (α × α)

One can use attribute [local instance] Sym2.Rel.setoid to temporarily make Quotient functionality work for α × α.

@[simp]

theorem Sym2.rel_iff' {α : Type u_1} {p q : α × α} : Rel α p q ↔ p = q ∨ p = q.swap

theorem Sym2.rel_iff {α : Type u_1} {x y z w : α} : Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

@[reducible, inline]

abbrev Sym2 (α : Type u) : Type u

Sym2 α is the symmetric square of α, which, in other words, is the type of unordered pairs.

It is equivalent in a natural way to multisets of cardinality 2 (see Sym2.equivMultiset).

@[reducible, inline]

abbrev Sym2.mk {α : Type u_4} (a b : α) : Sym2 α

Constructor for Sym2. This is the quotient map α × α → Sym2 α.

def «termS(_,_)» : Lean.ParserDescr

s(x, y) is an unordered pair, which is to say a pair modulo the action of the symmetric group.

It is equal to Sym2.mk (x, y).

theorem Sym2.sound {α : Type u_1} {a b c d : α} (h : Rel α (a, b) (c, d)) : s(a, b) = s(c, d)

theorem Sym2.exact {α : Type u_1} {a b c d : α} (h : s(a, b) = s(c, d)) : Rel α (a, b) (c, d)

@[simp]

theorem Sym2.eq {α : Type u_1} {a b c d : α} : s(a, b) = s(c, d) ↔ Rel α (a, b) (c, d)

theorem Sym2.ind {α : Type u_1} {f : Sym2 α → Prop} (h : ∀ (x y : α), f s(x, y)) (i : Sym2 α) : f i

theorem Sym2.inductionOn {α : Type u_1} {f : Sym2 α → Prop} (i : Sym2 α) (hf : ∀ (x y : α), f s(x, y)) : f i

theorem Sym2.inductionOn₂ {α : Type u_1} {β : Type u_2} {f : Sym2 α → Sym2 β → Prop} (i : Sym2 α) (j : Sym2 β) (hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)) : f i j

def Sym2.rec {α : Type u_1} {motive : Sym2 α → Sort u_4} (f : (a b : α) → motive s(a, b)) (h : ∀ (a b c d : α) (h : Rel α (a, b) (c, d)), ⋯ ▸ f a b = f c d) (z : Sym2 α) : motive z

Dependent recursion principle for Sym2. See Quot.rec.

def Sym2.recOn {α : Type u_1} {motive : Sym2 α → Sort u_4} (z : Sym2 α) (f : (a b : α) → motive s(a, b)) (h : ∀ (a b c d : α) (h : Rel α (a, b) (c, d)), ⋯ ▸ f a b = f c d) : motive z

Dependent recursion principle for Sym2. See Quot.recOn.

def Sym2.hrec {α : Type u_1} {motive : Sym2 α → Sort u_4} (f : (a b : α) → motive s(a, b)) (h : ∀ (a b : α), f a b ≍ f b a) (z : Sym2 α) : motive z

A dependent recursion principle for Sym2 that uses heterogeneous equality.

@[reducible, inline]

abbrev Sym2.recOnSubsingleton {α : Type u_1} {motive : Sym2 α → Sort u_4} [∀ (a b : α), Subsingleton (motive s(a, b))] (z : Sym2 α) (f : (a b : α) → motive s(a, b)) : motive z

Dependent recursion principal for Sym2 when the target is a Subsingleton type. See Quot.recOnSubsingleton.

theorem Sym2.mk_surjective {α : Type u_1} : Function.Surjective (Function.uncurry Sym2.mk)

theorem Sym2.exists {α : Type u_4} {f : Sym2 α → Prop} : (∃ (x : Sym2 α), f x) ↔ ∃ (x : α) (y : α), f s(x, y)

theorem Sym2.forall {α : Type u_4} {f : Sym2 α → Prop} : (∀ (x : Sym2 α), f x) ↔ ∀ (x y : α), f s(x, y)

theorem Sym2.eq_swap {α : Type u_1} {a b : α} : s(a, b) = s(b, a)

@[deprecated Sym2.eq_swap (since := "2026-02-05")]

theorem Sym2.mk_prod_swap_eq {α : Type u_1} {a b : α} : s(a, b) = s(b, a)

Alias of Sym2.eq_swap.

theorem Sym2.congr_right {α : Type u_1} {a b c : α} : s(a, b) = s(a, c) ↔ b = c

theorem Sym2.congr_left {α : Type u_1} {a b c : α} : s(b, a) = s(c, a) ↔ b = c

theorem Sym2.eq_iff {α : Type u_1} {x y z w : α} : s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

theorem Sym2.mk_eq_mk_iff {α : Type u_1} {p q : α × α} : s(p.1, p.2) = s(q.1, q.2) ↔ p = q ∨ p = q.swap

def Sym2.lift {α : Type u_1} {β : Type u_2} : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ } ≃ (Sym2 α → β)

The universal property of Sym2; symmetric functions of two arguments are equivalent to functions from Sym2. Note that when β is Prop, it can sometimes be more convenient to use Sym2.fromRel instead.

@[simp]

theorem Sym2.lift_mk {α : Type u_1} {β : Type u_2} (f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (a b : α) : lift f s(a, b) = ↑f a b

@[simp]

theorem Sym2.coe_lift_symm_apply {α : Type u_1} {β : Type u_2} (F : Sym2 α → β) (a₁ a₂ : α) : ↑(lift.symm F) a₁ a₂ = F s(a₁, a₂)

def Sym2.lift₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} : { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ } ≃ (Sym2 α → Sym2 β → γ)

A two-argument version of Sym2.lift.

@[simp]

theorem Sym2.lift₂_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) (a₁ a₂ : α) (b₁ b₂ : β) : lift₂ f s(a₁, a₂) s(b₁, b₂) = ↑f a₁ a₂ b₁ b₂

@[simp]

theorem Sym2.coe_lift₂_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F : Sym2 α → Sym2 β → γ) (a₁ a₂ : α) (b₁ b₂ : β) : ↑(lift₂.symm F) a₁ a₂ b₁ b₂ = F s(a₁, a₂) s(b₁, b₂)

def Sym2.map {α : Type u_1} {β : Type u_2} (f : α → β) : Sym2 α → Sym2 β

The functor Sym2 is functorial, and this function constructs the induced maps.

@[simp]

theorem Sym2.map_id {α : Type u_1} : map id = id

theorem Sym2.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} : map (g ∘ f) = map g ∘ map f

theorem Sym2.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} (x : Sym2 α) : map g (map f x) = map (g ∘ f) x

@[simp]

theorem Sym2.map_mk {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α) : map f s(a, b) = s(f a, f b)

@[deprecated Sym2.map_mk (since := "2026-02-05")]

theorem Sym2.map_pair_eq {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α) : map f s(a, b) = s(f a, f b)

Alias of Sym2.map_mk.

theorem Sym2.map.injective {α : Type u_1} {β : Type u_2} {f : α → β} (hinj : Function.Injective f) : Function.Injective (map f)

def Sym2.mkEmbedding {α : Type u_1} (a : α) : α ↪ Sym2 α

mk a as an embedding. This is the symmetric version of Function.Embedding.sectL.

@[simp]

theorem Sym2.mkEmbedding_apply {α : Type u_1} (a b : α) : (mkEmbedding a) b = s(a, b)

def Function.Embedding.sym2Map {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Sym2 α ↪ Sym2 β

Sym2.map as an embedding.

@[simp]

theorem Function.Embedding.sym2Map_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a✝ : Sym2 α) : f.sym2Map a✝ = Sym2.map (⇑f) a✝

theorem Sym2.lift_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) : lift f ∘ map g = lift ⟨fun (c₁ c₂ : γ) => ↑f (g c₁) (g c₂), ⋯⟩

theorem Sym2.lift_map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (p : Sym2 γ) : lift f (map g p) = lift ⟨fun (c₁ c₂ : γ) => ↑f (g c₁) (g c₂), ⋯⟩ p

Membership and set coercion

def Sym2.Mem {α : Type u_1} (x : α) (z : Sym2 α) : Prop

This is a predicate that determines whether a given term is a member of a term of the symmetric square. From this point of view, the symmetric square is the subtype of cardinality-two multisets on α.

theorem Sym2.mem_iff' {α : Type u_1} {a b c : α} : Sym2.Mem a s(b, c) ↔ a = b ∨ a = c

@[implicit_reducible]

instance Sym2.instSetLike {α : Type u_1} : SetLike (Sym2 α) α

@[implicit_reducible]

instance Sym2.instPartialOrder {α : Type u_1} : PartialOrder (Sym2 α)

@[simp]

theorem Sym2.mem_iff_mem {α : Type u_1} {x : α} {z : Sym2 α} : Sym2.Mem x z ↔ x ∈ z

theorem Sym2.mem_iff_exists {α : Type u_1} {x : α} {z : Sym2 α} : x ∈ z ↔ ∃ (y : α), z = s(x, y)

theorem Sym2.ext {α : Type u_1} {p q : Sym2 α} (h : ∀ (x : α), x ∈ p ↔ x ∈ q) : p = q

theorem Sym2.ext_iff {α : Type u_1} {p q : Sym2 α} : p = q ↔ ∀ (x : α), x ∈ p ↔ x ∈ q

theorem Sym2.mem_mk_left {α : Type u_1} (x y : α) : x ∈ s(x, y)

theorem Sym2.mem_mk_right {α : Type u_1} (x y : α) : y ∈ s(x, y)

@[simp]

theorem Sym2.mem_iff {α : Type u_1} {a b c : α} : a ∈ s(b, c) ↔ a = b ∨ a = c

theorem Sym2.out_fst_mem {α : Type u_1} (e : Sym2 α) : (Quot.out e).1 ∈ e

theorem Sym2.out_snd_mem {α : Type u_1} (e : Sym2 α) : (Quot.out e).2 ∈ e

theorem Sym2.ball {α : Type u_1} {p : α → Prop} {a b : α} : (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

@[simp]

theorem Sym2.coe_mk {α : Type u_1} {x y : α} : ↑s(x, y) = {x, y}

theorem Sym2.coe_map {α : Type u_1} {β : Type u_2} (f : α → β) (z : Sym2 α) : ↑(map f z) = f '' ↑z

noncomputable def Sym2.Mem.other {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z) : α

Given an element of the unordered pair, give the other element using Classical.choose. See also Mem.other' for the computable version.

@[simp]

theorem Sym2.other_spec {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z) : s(a, Mem.other h) = z

theorem Sym2.other_mem {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other h ∈ z

theorem Sym2.mem_and_mem_iff {α : Type u_1} {x y : α} {z : Sym2 α} (hne : x ≠ y) : x ∈ z ∧ y ∈ z ↔ z = s(x, y)

theorem Sym2.eq_of_ne_mem {α : Type u_1} {x y : α} {z z' : Sym2 α} (h : x ≠ y) (h1 : x ∈ z) (h2 : y ∈ z) (h3 : x ∈ z') (h4 : y ∈ z') : z = z'

@[implicit_reducible]

instance Sym2.Mem.decidable {α : Type u_1} [DecidableEq α] (x : α) (z : Sym2 α) : Decidable (x ∈ z)

@[simp]

theorem Sym2.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {z : Sym2 α} : b ∈ map f z ↔ ∃ a ∈ z, f a = b

theorem Sym2.map_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Sym2 α} (h : ∀ x ∈ s, f x = g x) : map f s = map g s

@[simp]

theorem Sym2.map_id' {α : Type u_1} : (map fun (x : α) => x) = id

Note: Sym2.map_id will not simplify Sym2.map id z due to Sym2.map_congr.

def Sym2.pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (s : Sym2 α) : (∀ a ∈ s, P a) → Sym2 β

Partial map. If f : ∀ a, p a → β is a partial function defined on a : α satisfying p, then pmap f s h is essentially the same as map f s but is defined only when all members of s satisfy p, using the proof to apply f.

theorem Sym2.forall_mem_pair {α : Type u_1} {P : α → Prop} {a b : α} : (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b

theorem Sym2.pair_eq_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (a b : α) (h : P a) (h' : P b) : s(f a h, f b h') = pmap f s(a, b) ⋯

theorem Sym2.pmap_pair {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (a b : α) (h : ∀ x ∈ s(a, b), P x) : pmap f s(a, b) h = s(f a ⋯, f b ⋯)

@[simp]

theorem Sym2.mem_pmap_iff {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) (b : β) : b ∈ pmap f z h ↔ ∃ (a : α) (ha : a ∈ z), b = f a ⋯

theorem Sym2.pmap_eq_map {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : α → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) : pmap (fun (a : α) (x : P a) => f a) z h = map f z

theorem Sym2.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Q : β → Prop} (f : α → β) (g : (b : β) → Q b → γ) (z : Sym2 α) (h : ∀ b ∈ map f z, Q b) : pmap g (map f z) h = pmap (fun (a : α) (ha : a ∈ z) => g (f a) ⋯) z ⋯

theorem Sym2.pmap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {P : α → Prop} {Q : β → Prop} (f : (a : α) → P a → β) (g : β → γ) (z : Sym2 α) (h : ∀ a ∈ z, P a) (h' : ∀ b ∈ pmap f z h, Q b) : map g (pmap f z h) = pmap (fun (a : α) (ha : a ∈ z) => g (f a ⋯)) z ⋯

theorem Sym2.pmap_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {P : α → Prop} {Q : β → Prop} (f : (a : α) → P a → β) (g : (b : β) → Q b → γ) (z : Sym2 α) (h : ∀ a ∈ z, P a) (h' : ∀ b ∈ pmap f z h, Q b) : pmap g (pmap f z h) h' = pmap (fun (a : α) (ha : a ∈ z) => g (f a ⋯) ⋯) z ⋯

@[simp]

theorem Sym2.pmap_subtype_map_subtypeVal {α : Type u_1} {P : α → Prop} (s : Sym2 α) (h : ∀ a ∈ s, P a) : map Subtype.val (pmap Subtype.mk s h) = s

def Sym2.attachWith {α : Type u_1} {P : α → Prop} (s : Sym2 α) (h : ∀ a ∈ s, P a) : Sym2 { a : α // P a }

"Attach" a proof P a that holds for all the elements of s to produce a new Sym2 object with the same elements but in the type {x // P x}.

@[simp]

theorem Sym2.attachWith_map_subtypeVal {α : Type u_1} {s : Sym2 α} {P : α → Prop} (h : ∀ a ∈ s, P a) : map Subtype.val (s.attachWith h) = s

Diagonal

def Sym2.diag {α : Type u_1} (x : α) : Sym2 α

A type α is naturally included in the diagonal of α × α, and this function gives the image of this diagonal in Sym2 α.

theorem Sym2.diag_injective {α : Type u_1} : Function.Injective diag

def Sym2.IsDiag {α : Type u_1} : Sym2 α → Prop

A predicate for testing whether an element of Sym2 α is on the diagonal.

@[simp]

theorem Sym2.mk_isDiag_iff {α : Type u_1} {x y : α} : s(x, y).IsDiag ↔ x = y

@[deprecated Sym2.mk_isDiag_iff (since := "2026-02-05")]

theorem Sym2.isDiag_iff_proj_eq {α : Type u_1} {x y : α} : s(x, y).IsDiag ↔ x = y

Alias of Sym2.mk_isDiag_iff.

theorem Sym2.IsDiag.map {α : Type u_1} {β : Type u_2} {z : Sym2 α} {f : α → β} : z.IsDiag → (map f z).IsDiag

theorem Sym2.isDiag_map {α : Type u_1} {β : Type u_2} {z : Sym2 α} {f : α → β} (hf : Function.Injective f) : (map f z).IsDiag ↔ z.IsDiag

@[simp]

theorem Sym2.diag_isDiag {α : Type u_1} (a : α) : (diag a).IsDiag

@[simp]

theorem Sym2.isDiag_of_subsingleton {α : Type u_1} [Subsingleton α] (z : Sym2 α) : z.IsDiag

def Sym2.diagSet {α : Type u_1} : Set (Sym2 α)

The set of all Sym2 α elements on the diagonal.

@[simp]

theorem Sym2.mem_diagSet {α : Type u_1} {z : Sym2 α} : z ∈ diagSet ↔ z.IsDiag

@[deprecated Sym2.mem_diagSet (since := "2025-12-10")]

theorem Sym2.mem_diagSet_iff_isDiag {α : Type u_1} (z : Sym2 α) : z ∈ diagSet ↔ z.IsDiag

@[simp]

theorem Sym2.range_diag {α : Type u_1} : Set.range diag = diagSet

@[deprecated Sym2.mem_diagSet_iff_isDiag (since := "2025-11-05")]

theorem Sym2.IsDiag.mem_range_diag {α : Type u_1} (z : Sym2 α) : z.IsDiag → z ∈ diagSet

Alias of the reverse direction of Sym2.mem_diagSet_iff_isDiag.

@[deprecated Sym2.range_diag (since := "2025-11-05")]

theorem Sym2.isDiag_iff_mem_range_diag {α : Type u_1} (z : Sym2 α) : z.IsDiag ↔ z ∈ Set.range diag

@[deprecated Sym2.mem_diagSet (since := "2025-11-05")]

theorem Sym2.mem_diagSet_iff_eq {α : Type u_1} {a b : α} : s(a, b) ∈ diagSet ↔ a = b

theorem Sym2.diagSet_eq_setOf_isDiag {α : Type u_1} : diagSet = {z : Sym2 α | z.IsDiag}

@[deprecated Set.compl_setOf (since := "2025-12-10")]

theorem Sym2.diagSet_compl_eq_setOf_not_isDiag {α : Type u_1} : diagSetᶜ = {z : Sym2 α | ¬z.IsDiag}

theorem Sym2.diagSet_eq_univ_of_subsingleton {α : Type u_1} [Subsingleton α] : diagSet = Set.univ

@[implicit_reducible]

instance Sym2.IsDiag.decidablePred (α : Type u) [DecidableEq α] : DecidablePred IsDiag

@[implicit_reducible]

instance Sym2.decidablePred_mem_diagSet (α : Type u) [DecidableEq α] : DecidablePred fun (x : Sym2 α) => x ∈ diagSet

theorem Sym2.other_ne {α : Type u_1} {a : α} {z : Sym2 α} (hd : ¬z.IsDiag) (h : a ∈ z) : Mem.other h ≠ a

Declarations about symmetric relations

def Sym2.fromRel {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) : Set (Sym2 α)

Symmetric relations define a set on Sym2 α by taking all those pairs of elements that are related.

@[simp]

theorem Sym2.fromRel_prop {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {a b : α} : s(a, b) ∈ fromRel sym ↔ r a b

@[deprecated Sym2.fromRel_prop (since := "2026-02-05")]

theorem Sym2.fromRel_proj_prop {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {a b : α} : s(a, b) ∈ fromRel sym ↔ r a b

Alias of Sym2.fromRel_prop.

theorem Sym2.fromRel_mono_iff {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Symmetric r₁) (sym₂ : Symmetric r₂) : fromRel sym₁ ⊆ fromRel sym₂ ↔ r₁ ≤ r₂

theorem Sym2.fromRel_mono {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Symmetric r₁) (sym₂ : Symmetric r₂) : r₁ ≤ r₂ → fromRel sym₁ ⊆ fromRel sym₂

Alias of the reverse direction of Sym2.fromRel_mono_iff.

theorem Sym2.fromRel_bot {α : Type u_1} : fromRel ⋯ = ∅

@[simp]

theorem Sym2.fromRel_bot_iff {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} : fromRel sym = ∅ ↔ r = ⊥

theorem Sym2.fromRel_top {α : Type u_1} : fromRel ⋯ = Set.univ

@[simp]

theorem Sym2.fromRel_top_iff {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} : fromRel sym = Set.univ ↔ r = ⊤

theorem Sym2.fromRel_ne {α : Type u_1} : fromRel ⋯ = {z : Sym2 α | ¬z.IsDiag}

theorem Sym2.diagSet_eq_fromRel_eq {α : Type u_1} : diagSet = fromRel ⋯

theorem Sym2.diagSet_compl_eq_fromRel_ne {α : Type u_1} : diagSetᶜ = fromRel ⋯

@[simp]

theorem Sym2.diagSet_subset_fromRel {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) : diagSet ⊆ fromRel hr ↔ Reflexive r

@[simp]

theorem Sym2.disjoint_diagSet_fromRel {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) : Disjoint diagSet (fromRel hr) ↔ Std.Irrefl r

@[simp]

theorem Sym2.fromRel_subset_compl_diagSet {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) : fromRel hr ⊆ diagSetᶜ ↔ Std.Irrefl r

@[deprecated Sym2.diagSet_subset_fromRel (since := "2025-12-10")]

theorem Sym2.reflexive_iff_diagSet_subset_fromRel {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) : Reflexive r ↔ diagSet ⊆ fromRel sym

@[deprecated Sym2.fromRel_subset_compl_diagSet (since := "2025-12-10")]

theorem Sym2.irreflexive_iff_fromRel_subset_diagSet_compl {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) : Std.Irrefl r ↔ fromRel sym ⊆ diagSetᶜ

theorem Sym2.fromRel_irrefl {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} : Std.Irrefl r ↔ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

@[deprecated Sym2.fromRel_irrefl (since := "2026-02-12")]

theorem Sym2.fromRel_irreflexive {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} : Std.Irrefl r ↔ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Alias of Sym2.fromRel_irrefl.

theorem Sym2.mem_fromRel_irrefl_other_ne {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} (irrefl : Std.Irrefl r) {a : α} {z : Sym2 α} (hz : z ∈ fromRel sym) (h : a ∈ z) : Mem.other h ≠ a

@[implicit_reducible]

instance Sym2.fromRel.decidablePred {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) [h : DecidableRel r] : DecidablePred fun (x : Sym2 α) => x ∈ fromRel sym

theorem Sym2.fromRel_relationMap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (hr : Symmetric r) (f : α → β) : fromRel ⋯ = map f '' fromRel hr

def Sym2.ToRel {α : Type u_1} (s : Set (Sym2 α)) (x y : α) : Prop

The inverse to Sym2.fromRel. Given a set on Sym2 α, give a symmetric relation on α (see Sym2.toRel_symmetric).

@[simp]

theorem Sym2.toRel_prop {α : Type u_1} (s : Set (Sym2 α)) (x y : α) : ToRel s x y ↔ s(x, y) ∈ s

theorem Sym2.toRel_symmetric {α : Type u_1} (s : Set (Sym2 α)) : Symmetric (ToRel s)

theorem Sym2.toRel_fromRel {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) : ToRel (fromRel sym) = r

theorem Sym2.fromRel_toRel {α : Type u_1} (s : Set (Sym2 α)) : fromRel ⋯ = s

theorem Sym2.toRel_mono_iff {α : Type u_1} (s₁ s₂ : Set (Sym2 α)) : ToRel s₁ ≤ ToRel s₂ ↔ s₁ ⊆ s₂

theorem Sym2.toRel_mono {α : Type u_1} (s₁ s₂ : Set (Sym2 α)) : s₁ ⊆ s₂ → ToRel s₁ ≤ ToRel s₂

Alias of the reverse direction of Sym2.toRel_mono_iff.

def Sym2.toRelOrderEmbedding (α : Type u_1) : Set (Sym2 α) ↪o (α → α → Prop)

ToRel induces an order embedding from Sym2 sets to relations

def Sym2.fromRelOrderIso (α : Type u_1) : { r : α → α → Prop // Symmetric r } ≃o Set (Sym2 α)

fromRel/ToRel induce an order isomorphism between symmetric relations and Sym2 sets

@[simp]

theorem Sym2.fromRelOrderIso_symm_apply_coe (α : Type u_1) (s : Set (Sym2 α)) (x y : α) : ↑((RelIso.symm (fromRelOrderIso α)) s) x y = ToRel s x y

@[simp]

theorem Sym2.fromRelOrderIso_apply (α : Type u_1) (r : { r : α → α → Prop // Symmetric r }) : (fromRelOrderIso α) r = fromRel ⋯

@[deprecated Sym2.fromRelOrderIso (since := "2026-03-11")]

def Sym2.fromRelOrderEmbedding {α : Type u_1} : { r : α → α → Prop // Symmetric r } ↪o Set (Sym2 α)

fromRel induces an order embedding from symmetric relations to Sym2 sets.

@[simp]

theorem Sym2.fromRel_eq_fromRel_iff_eq {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Symmetric r₁) (sym₂ : Symmetric r₂) : fromRel sym₁ = fromRel sym₂ ↔ r₁ = r₂

@[deprecated Sym2.fromRel_eq_fromRel_iff_eq (since := "2026-03-11")]

theorem Sym2.fromRel_eq_fromRell_iff_eq {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Symmetric r₁) (sym₂ : Symmetric r₂) : fromRel sym₁ = fromRel sym₂ ↔ r₁ = r₂

Alias of Sym2.fromRel_eq_fromRel_iff_eq.

def Sym2.toMultiset {α : Type u_4} (z : Sym2 α) : Multiset α

Map an unordered pair to an unordered list.

theorem Sym2.card_toMultiset {α : Type u_4} (z : Sym2 α) : z.toMultiset.card = 2

Mapping an unordered pair to an unordered list produces a multiset of size 2.

@[simp]

theorem Sym2.mem_toMultiset {α : Type u_4} {x : α} {z : Sym2 α} : x ∈ z.toMultiset ↔ x ∈ z

The members of an unordered pair are members of the corresponding unordered list.

def Sym2.toFinset {α : Type u_1} [DecidableEq α] (z : Sym2 α) : Finset α

Map an unordered pair to a finite set.

@[simp]

theorem Sym2.mem_toFinset {α : Type u_1} [DecidableEq α] {x : α} {z : Sym2 α} : x ∈ z.toFinset ↔ x ∈ z

The members of an unordered pair are members of the corresponding finite set.

@[simp]

theorem Sym2.toFinset_ne_empty {α : Type u_1} [DecidableEq α] (z : Sym2 α) : z.toFinset ≠ ∅

theorem Sym2.toFinset_mk_eq {α : Type u_1} [DecidableEq α] {x y : α} : s(x, y).toFinset = {x, y}

theorem Sym2.card_toFinset_of_isDiag {α : Type u_1} [DecidableEq α] (z : Sym2 α) (h : z.IsDiag) : z.toFinset.card = 1

Mapping an unordered pair on the diagonal to a finite set produces a finset of size 1.

theorem Sym2.card_toFinset_of_not_isDiag {α : Type u_1} [DecidableEq α] (z : Sym2 α) (h : ¬z.IsDiag) : z.toFinset.card = 2

Mapping an unordered pair off the diagonal to a finite set produces a finset of size 2.

theorem Sym2.card_toFinset {α : Type u_1} [DecidableEq α] (z : Sym2 α) : z.toFinset.card = if z.IsDiag then 1 else 2

Mapping an unordered pair to a finite set produces a finset of size 1 if the pair is on the diagonal, else of size 2 if the pair is off the diagonal.

Equivalence to the second symmetric power

def Sym2.sym2EquivSym' {α : Type u_1} : Sym2 α ≃ Sym.Sym' α 2

The symmetric square is equivalent to length-2 vectors up to permutations.

def Sym2.equivSym (α : Type u_4) : Sym2 α ≃ Sym α 2

The symmetric square is equivalent to the second symmetric power.

def Sym2.equivMultiset (α : Type u_4) : Sym2 α ≃ { s : Multiset α // s.card = 2 }

The symmetric square is equivalent to multisets of cardinality two. (This is currently a synonym for equivSym, but it's provided in case the definition for Sym changes.)

@[implicit_reducible]

instance Sym2.instDecidableRel {α : Type u_1} [DecidableEq α] : DecidableRel (Rel α)

Given [DecidableEq α] and [Fintype α], the following instance gives Fintype (Sym2 α).

@[implicit_reducible]

instance Sym2.instDecidableRel' {α : Type u_1} [DecidableEq α] : DecidableRel HasEquiv.Equiv

@[implicit_reducible]

instance Sym2.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Sym2 α)

The other element of an element of the symmetric square

def Sym2.Mem.other' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : α

Get the other element of the unordered pair using the decidable equality. This is the computable version of Mem.other.

@[simp]

theorem Sym2.other_spec' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : s(a, Mem.other' h) = z

@[simp]

theorem Sym2.other_eq_other' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other h = Mem.other' h

theorem Sym2.other_mem' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other' h ∈ z

theorem Sym2.other_invol' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Mem.other' ha ∈ z) : Mem.other' hb = a

theorem Sym2.other_invol {α : Type u_1} {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Mem.other ha ∈ z) : Mem.other hb = a

theorem Sym2.filter_image_mk_isDiag {α : Type u_1} [DecidableEq α] (s : Finset α) : {x ∈ Finset.image (Function.uncurry Sym2.mk) (s ×ˢ s) | x.IsDiag} = Finset.image (Function.uncurry Sym2.mk) s.diag

theorem Sym2.filter_image_mk_not_isDiag {α : Type u_1} [DecidableEq α] (s : Finset α) : {x ∈ Finset.image (Function.uncurry Sym2.mk) (s ×ˢ s) | ¬x.IsDiag} = Finset.image (Function.uncurry Sym2.mk) s.offDiag

instance Sym2.instSubsingleton {α : Type u_1} [Subsingleton α] : Subsingleton (Sym2 α)

@[implicit_reducible]

instance Sym2.instUnique {α : Type u_1} [Unique α] : Unique (Sym2 α)

instance Sym2.instIsEmpty {α : Type u_1} [IsEmpty α] : IsEmpty (Sym2 α)

instance Sym2.instNontrivial {α : Type u_1} [Nontrivial α] : Nontrivial (Sym2 α)

@[implicit_reducible]

unsafe instance Sym2.instRepr {α : Type u_1} [Repr α] : Repr (Sym2 α)

theorem Sym2.lift_smul_lift {α : Type u_4} {R : Type u_5} {N : Type u_6} [SMul R N] (f : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (g : { g : α → α → N // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }) : lift f • lift g = lift ⟨↑f • ↑g, ⋯⟩

def Sym2.mul {M : Type u_4} [CommMagma M] : Sym2 M → M

Multiplication as a function from Sym2.

def Sym2.add {M : Type u_4} [AddCommMagma M] : Sym2 M → M

Addition as a function from Sym2.

@[simp]

theorem Sym2.mul_mk {M : Type u_4} [CommMagma M] (a b : M) : s(a, b).mul = a * b

@[simp]

theorem Sym2.add_mk {M : Type u_4} [AddCommMagma M] (a b : M) : s(a, b).add = a + b

def Set.sym2 {α : Type u_1} (s : Set α) : Set (Sym2 α)

For a set s : Set α, s.sym2 is the set of all unordered pairs of elements from s.

@[simp]

theorem Set.mk_mem_sym2_iff {α : Type u_1} {s : Set α} {x y : α} : s(x, y) ∈ s.sym2 ↔ x ∈ s ∧ y ∈ s

@[deprecated Set.mk_mem_sym2_iff (since := "2026-02-05")]

theorem Set.mk'_mem_sym2_iff {α : Type u_1} {s : Set α} {x y : α} : s(x, y) ∈ s.sym2 ↔ x ∈ s ∧ y ∈ s

Alias of Set.mk_mem_sym2_iff.

theorem Set.mem_sym2_iff_subset {α : Type u_1} {s : Set α} {z : Sym2 α} : z ∈ s.sym2 ↔ ↑z ⊆ s

theorem Set.sym2_eq_mk_image {α : Type u_1} {s : Set α} : s.sym2 = Function.uncurry Sym2.mk '' s ×ˢ s

@[simp]

theorem Set.mk_preimage_sym2 {α : Type u_1} {s : Set α} : Function.uncurry Sym2.mk ⁻¹' s.sym2 = s ×ˢ s

@[simp]

theorem Set.sym2_empty {α : Type u_1} : ∅.sym2 = ∅

@[simp]

theorem Set.sym2_univ {α : Type u_1} : univ.sym2 = univ

@[simp]

theorem Set.sym2_singleton {α : Type u_1} (a : α) : {a}.sym2 = {s(a, a)}

theorem Set.sym2_insert {α : Type u_1} (a : α) (s : Set α) : (insert a s).sym2 = (fun (b : α) => s(a, b)) '' insert a s ∪ s.sym2

theorem Set.sym2_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : (f ⁻¹' s).sym2 = Sym2.map f ⁻¹' s.sym2

theorem Set.sym2_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : (f '' s).sym2 = Sym2.map f '' s.sym2

theorem Set.sym2_inter {α : Type u_1} (s t : Set α) : (s ∩ t).sym2 = s.sym2 ∩ t.sym2

theorem Set.sym2_iInter {α : Type u_1} {ι : Type u_4} (f : ι → Set α) : (⋂ (i : ι), f i).sym2 = ⋂ (i : ι), (f i).sym2