instance Sym2.decBall {α : Type} (p : α → Prop) [pdec : DecidablePred p] (s : Sym2 α) : Decidable (∀ x ∈ s, p x)

Equations

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

instance Sym2.decBex {α : Type} (p : α → Prop) [pdec : DecidablePred p] (s : Sym2 α) : Decidable (∃ x ∈ s, p x)

Equations

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

def Sym2.toOrderedPair {α : Type} [LinearOrder α] (s : Sym2 α) : α × α

Equations

• s.toOrderedPair = Sym2.rec (fun (p : α × α) => (min p.1 p.2, max p.1 p.2)) ⋯ s

theorem Sym2.exists_mem_pair {α : Type u_1} {P : α → Prop} {a b : α} : (∃ x ∈ s(a, b), P x) ↔ P a ∨ P b

theorem Sym2.toOrderedPair_repr {α : Type} [LinearOrder α] (s : Sym2 α) : s = s(s.toOrderedPair.1, s.toOrderedPair.2)

theorem Sym2.toOrderedPair_inj {α : Type} [LinearOrder α] : Function.Injective toOrderedPair

theorem Sym2.toOrderedPair_IsDiag_of_eq {α : Type} [inst : LinearOrder α] {s t : Sym2 α} : s.toOrderedPair = t.toOrderedPair.swap → s.IsDiag ∧ t.IsDiag

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