Documentation

Mathlib.Data.Sym.Sym2

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∈ 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 symmetric square has a setoid instance, so ⟦(a, b)⟧ denotes a term of the symmetric square.

Tags #

symmetric square, unordered pairs, symmetric powers

inductive Sym2.Rel (α : Type u) :

α × α → α × α → Prop

refl: ∀ {α : Type u} (x y : α), Sym2.Rel α (x, y) (x, y)
swap: ∀ {α : Type u} (x y : α), Sym2.Rel α (x, y) (y, x)

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

Instances For

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

Sym2.Rel α x y → Sym2.Rel α y x

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

Sym2.Rel α x z

theorem Sym2.Rel.is_equivalence {α : Type u_1} :

Equivalence (Sym2.Rel α)

instance Sym2.Rel.setoid (α : Type u) :

Setoid (α × α)

Equations

Sym2.Rel.setoid α = { r := Sym2.Rel α, iseqv := (_ : Equivalence (Sym2.Rel α)) }

@[simp]

theorem Sym2.rel_iff {α : Type u_1} {x : α} {y : α} {z : α} {w : α} :

(x, y) ≈ (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

def Sym2 (α : 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).

Equations

Sym2 α = Quotient (Sym2.Rel.setoid α)

theorem Sym2.ind {α : Type u_1} {f : Sym2 α → Prop} (h : (x y : α) → f (Quotient.mk (Sym2.Rel.setoid α) (x, y))) (i : Sym2 α) :

f i

theorem Sym2.inductionOn {α : Type u_1} {f : Sym2 α → Prop} (i : Sym2 α) (hf : (x y : α) → f (Quotient.mk (Sym2.Rel.setoid α) (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 (Quotient.mk (Sym2.Rel.setoid α) (a₁, a₂)) (Quotient.mk (Sym2.Rel.setoid β) (b₁, b₂))) :

f i j

theorem Sym2.exists {α : Type u_1} {f : Sym2 α → Prop} :

(∃ x, f x) ↔ ∃ x y, f (Quotient.mk (Sym2.Rel.setoid α) (x, y))

theorem Sym2.forall {α : Type u_1} {f : Sym2 α → Prop} :

((x : Sym2 α) → f x) ↔ (x y : α) → f (Quotient.mk (Sym2.Rel.setoid α) (x, y))

theorem Sym2.eq_swap {α : Type u_1} {a : α} {b : α} :

Quotient.mk (Sym2.Rel.setoid α) (a, b) = Quotient.mk (Sym2.Rel.setoid α) (b, a)

@[simp]

theorem Sym2.mk''_prod_swap_eq {α : Type u_1} {p : α × α} :

Quotient.mk (Sym2.Rel.setoid α) (Prod.swap p) = Quotient.mk (Sym2.Rel.setoid α) p

theorem Sym2.congr_right {α : Type u_1} {a : α} {b : α} {c : α} :

Quotient.mk (Sym2.Rel.setoid α) (a, b) = Quotient.mk (Sym2.Rel.setoid α) (a, c) ↔ b = c

theorem Sym2.congr_left {α : Type u_1} {a : α} {b : α} {c : α} :

Quotient.mk (Sym2.Rel.setoid α) (b, a) = Quotient.mk (Sym2.Rel.setoid α) (c, a) ↔ b = c

theorem Sym2.eq_iff {α : Type u_1} {x : α} {y : α} {z : α} {w : α} :

Quotient.mk (Sym2.Rel.setoid α) (x, y) = Quotient.mk (Sym2.Rel.setoid α) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

theorem Sym2.mk''_eq_mk''_iff {α : Type u_1} {p : α × α} {q : α × α} :

Quotient.mk (Sym2.Rel.setoid α) p = Quotient.mk (Sym2.Rel.setoid α) q ↔ p = q ∨ p = Prod.swap q

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.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Sym2.lift_mk'' {α : Type u_1} {β : Type u_2} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (a₁ : α) (a₂ : α) :

↑Sym2.lift f (Quotient.mk (Sym2.Rel.setoid α) (a₁, a₂)) = ↑f a₁ a₂

@[simp]

theorem Sym2.coe_lift_symm_apply {α : Type u_1} {β : Type u_2} (F : Sym2 α → β) (a₁ : α) (a₂ : α) :

↑(↑(Equiv.symm Sym2.lift) F) a₁ a₂ = F (Quotient.mk (Sym2.Rel.setoid α) (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.

Equations

One or more equations did not get rendered due to their size.

@[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₂ : β) :

↑Sym2.lift₂ f (Quotient.mk (Sym2.Rel.setoid α) (a₁, a₂)) (Quotient.mk (Sym2.Rel.setoid β) (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₂ : β) :

↑(↑(Equiv.symm Sym2.lift₂) F) a₁ a₂ b₁ b₂ = F (Quotient.mk (Sym2.Rel.setoid α) (a₁, a₂)) (Quotient.mk (Sym2.Rel.setoid β) (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.

Equations

Sym2.map f = Quotient.map (Prod.map f f) (_ : ∀ ⦃a b : α × α⦄, a ≈ b → Prod.map f f a ≈ Prod.map f f b)

@[simp]

theorem Sym2.map_id {α : Type u_1} :

Sym2.map id = id

theorem Sym2.map_comp {α : Type u_1} {β : Type u_3} {γ : Type u_2} {g : β → γ} {f : α → β} :

Sym2.map (g ∘ f) = Sym2.map g ∘ Sym2.map f

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

Sym2.map g (Sym2.map f x) = Sym2.map (g ∘ f) x

@[simp]

theorem Sym2.map_pair_eq {α : Type u_2} {β : Type u_1} (f : α → β) (x : α) (y : α) :

Sym2.map f (Quotient.mk (Sym2.Rel.setoid α) (x, y)) = Quotient.mk (Sym2.Rel.setoid β) (f x, f y)

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

Function.Injective (Sym2.map f)

Membership and set coercion #

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

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 α.

Equations

Sym2.Mem x z = ∃ y, z = Quotient.mk (Sym2.Rel.setoid α) (x, y)

theorem Sym2.mem_iff' {α : Type u_1} {a : α} {b : α} {c : α} :

Sym2.Mem a (Quotient.mk (Sym2.Rel.setoid α) (b, c)) ↔ a = b ∨ a = c

instance Sym2.instSetLikeSym2 {α : Type u_1} :

SetLike (Sym2 α) α

Equations

One or more equations did not get rendered due to their size.

@[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 = Quotient.mk (Sym2.Rel.setoid α) (x, y)

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

p = q

theorem Sym2.mem_mk''_left {α : Type u_1} (x : α) (y : α) :

x ∈ Quotient.mk (Sym2.Rel.setoid α) (x, y)

theorem Sym2.mem_mk''_right {α : Type u_1} (x : α) (y : α) :

y ∈ Quotient.mk (Sym2.Rel.setoid α) (x, y)

@[simp]

theorem Sym2.mem_iff {α : Type u_1} {a : α} {b : α} {c : α} :

a ∈ Quotient.mk (Sym2.Rel.setoid α) (b, c) ↔ a = b ∨ a = c

theorem Sym2.out_fst_mem {α : Type u_1} (e : Sym2 α) :

(Quotient.out e).fst ∈ e

theorem Sym2.out_snd_mem {α : Type u_1} (e : Sym2 α) :

(Quotient.out e).snd ∈ e

theorem Sym2.ball {α : Type u_1} {p : α → Prop} {a : α} {b : α} :

((c : α) → c ∈ Quotient.mk (Sym2.Rel.setoid α) (a, b) → p c) ↔ p a ∧ p b

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.

Equations

Sym2.Mem.other h = Classical.choose h

@[simp]

theorem Sym2.other_spec {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z) :

Quotient.mk (Sym2.Rel.setoid α) (a, Sym2.Mem.other h) = z

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

Sym2.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 = Quotient.mk (Sym2.Rel.setoid α) (x, y)

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

z = z'

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

Decidable (x ∈ z)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Sym2.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {z : Sym2 α} :

b ∈ Sym2.map f z ↔ ∃ a, a ∈ z ∧ f a = b

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

Sym2.map f s = Sym2.map g s

@[simp]

theorem Sym2.map_id' {α : Type u_1} :

(Sym2.map fun x => x) = id

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

Diagonal #

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

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

Equations

Sym2.diag x = Quotient.mk (Sym2.Rel.setoid α) (x, x)

theorem Sym2.diag_injective {α : Type u_1} :

Function.Injective Sym2.diag

def Sym2.IsDiag {α : Type u_1} :

Sym2 α → Prop

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

Equations

Sym2.IsDiag = ↑Sym2.lift { val := Eq, property := (_ : ∀ (x x_1 : α), (x = x_1) = (x_1 = x)) }

theorem Sym2.mk''_isDiag_iff {α : Type u_1} {x : α} {y : α} :

Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) (x, y)) ↔ x = y

@[simp]

theorem Sym2.isDiag_iff_proj_eq {α : Type u_1} (z : α × α) :

Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) z) ↔ z.fst = z.snd

@[simp]

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

Sym2.IsDiag (Sym2.diag a)

theorem Sym2.IsDiag.mem_range_diag {α : Type u_1} {z : Sym2 α} :

Sym2.IsDiag z → z ∈ Set.range Sym2.diag

theorem Sym2.isDiag_iff_mem_range_diag {α : Type u_1} (z : Sym2 α) :

Sym2.IsDiag z ↔ z ∈ Set.range Sym2.diag

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

DecidablePred Sym2.IsDiag

Equations

Sym2.IsDiag.decidablePred α z = Quotient.recOnSubsingleton z fun a => Eq.mpr (_ : Decidable (Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)) = Decidable (a.fst = a.snd)) inferInstance

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

Sym2.Mem.other h ≠ a

Declarations about symmetric relations #

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

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

Equations

Sym2.fromRel sym = setOf (↑Sym2.lift { val := r, property := (_ : ∀ (x x_1 : α), r x x_1 = r x_1 x) })

@[simp]

theorem Sym2.fromRel_proj_prop {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {z : α × α} :

Quotient.mk (Sym2.Rel.setoid α) z ∈ Sym2.fromRel sym ↔ r z.fst z.snd

theorem Sym2.fromRel_prop {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {a : α} {b : α} :

Quotient.mk (Sym2.Rel.setoid α) (a, b) ∈ Sym2.fromRel sym ↔ r a b

theorem Sym2.fromRel_bot {α : Type u_1} :

(Sym2.fromRel fun x y => (_ : ⊥ x y → ⊥ x y)) = ∅

theorem Sym2.fromRel_top {α : Type u_1} :

(Sym2.fromRel fun x y => (_ : ⊤ x y → ⊤ x y)) = Set.univ

theorem Sym2.fromRel_irreflexive {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} :

Irreflexive r ↔ ∀ {z : Sym2 α}, z ∈ Sym2.fromRel sym → ¬Sym2.IsDiag z

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

Sym2.Mem.other h ≠ a

instance Sym2.fromRel.decidablePred {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) [h : DecidableRel r] :

DecidablePred fun x => x ∈ Sym2.fromRel sym

Equations

Sym2.fromRel.decidablePred sym z = Quotient.recOnSubsingleton z fun x => h x.fst x.snd

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

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

Equations

Sym2.ToRel s x y = (Quotient.mk (Sym2.Rel.setoid α) (x, y) ∈ s)

@[simp]

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

Sym2.ToRel s x y ↔ Quotient.mk (Sym2.Rel.setoid α) (x, y) ∈ s

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

Symmetric (Sym2.ToRel s)

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

Sym2.ToRel (Sym2.fromRel sym) = r

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

Sym2.fromRel (_ : Symmetric (Sym2.ToRel s)) = s

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.

Equations

One or more equations did not get rendered due to their size.

def Sym2.equivSym (α : Type u_1) :

Sym2 α ≃ Sym α 2

The symmetric square is equivalent to the second symmetric power.

Equations

Sym2.equivSym α = Equiv.trans Sym2.sym2EquivSym' (Equiv.symm Sym.symEquivSym')

def Sym2.equivMultiset (α : Type u_1) :

Sym2 α ≃ { s // ↑Multiset.card s = 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.)

Equations

Sym2.equivMultiset α = Sym2.equivSym α

def Sym2.relBool {α : Type u_1} [inst : DecidableEq α] (x : α × α) (y : α × α) :

An algorithm for computing Sym2.Rel.

Equations

Sym2.relBool x y = if x.fst = y.fst then decide (x.snd = y.snd) else if x.fst = y.snd then decide (x.snd = y.fst) else false

theorem Sym2.relBool_spec {α : Type u_1} [inst : DecidableEq α] (x : α × α) (y : α × α) :

Sym2.relBool x y = true ↔ Sym2.Rel α x y

instance Sym2.instDecidableRelProdRel (α : Type u_1) [inst : DecidableEq α] :

DecidableRel (Sym2.Rel α)

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

Equations

Sym2.instDecidableRelProdRel α x y = decidable_of_bool (Sym2.relBool x y) (_ : Sym2.relBool x y = true ↔ Sym2.Rel α x y)

def Sym2.eqBool {α : Type u_1} [inst : DecidableEq α] :

Sym2 α → Sym2 α → Bool

An algorithm for deciding equality in Sym2 α.

Equations

One or more equations did not get rendered due to their size.

theorem Sym2.eqBool_spec {α : Type u_1} [inst : DecidableEq α] (a : Sym2 α) (b : Sym2 α) :

Sym2.eqBool a b = true ↔ a = b

instance Sym2.instDecidableEqSym2 (α : Type u_1) [inst : DecidableEq α] :

DecidableEq (Sym2 α)

Equations

Sym2.instDecidableEqSym2 α a b = decidable_of_bool (Sym2.eqBool a b) (_ : Sym2.eqBool a b = true ↔ a = b)

The other element of an element of the symmetric square #

def Sym2.Mem.other' {α : Type u_1} [inst : 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.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Sym2.other_spec' {α : Type u_1} [inst : DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) :

Quotient.mk (Sym2.Rel.setoid α) (a, Sym2.Mem.other' h) = z

@[simp]

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

Sym2.Mem.other h = Sym2.Mem.other' h

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

Sym2.Mem.other' h ∈ z

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

Sym2.Mem.other' hb = a

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

Sym2.Mem.other hb = a

theorem Sym2.filter_image_quotient_mk''_isDiag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :

Finset.filter Sym2.IsDiag (Finset.image Quotient.mk'' (s ×ᶠ s)) = Finset.image Quotient.mk'' (Finset.diag s)

theorem Sym2.filter_image_quotient_mk''_not_isDiag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :

Finset.filter (fun a => ¬Sym2.IsDiag a) (Finset.image Quotient.mk'' (s ×ᶠ s)) = Finset.image Quotient.mk'' (Finset.offDiag s)

instance Sym2.instSubsingletonSym2 {α : Type u_1} [inst : Subsingleton α] :

Subsingleton (Sym2 α)

Equations

@Sym2.instSubsingletonSym2 = @Sym2.instSubsingletonSym2.proof_1

instance Sym2.instUniqueSym2 {α : Type u_1} [inst : Unique α] :

Unique (Sym2 α)

Equations

Sym2.instUniqueSym2 = Unique.mk' (Sym2 α)

instance Sym2.instIsEmptySym2 {α : Type u_1} [inst : IsEmpty α] :

IsEmpty (Sym2 α)

Equations

@Sym2.instIsEmptySym2 = @Sym2.instIsEmptySym2.proof_1

instance Sym2.instNontrivialSym2 {α : Type u_1} [inst : Nontrivial α] :

Nontrivial (Sym2 α)

Equations

@Sym2.instNontrivialSym2 = @Sym2.instNontrivialSym2.proof_1