Unordered-pair infrastructure

This file supplies elementary lemmas for transporting endpoint properties across equality of unordered pairs and for distinguishing unordered pairs by membership.

theorem Sym2.iff_iff_of_mk_eq {α : Type u_1} {P : α → Prop} {a b c d : α} (h : s(a, b) = s(c, d)) : (P a ↔ P b) ↔ (P c ↔ P d)

A property holds equivalently at the two ends of an unordered pair independently of the chosen ordering of those ends.

theorem Sym2.ne_of_mem_notMem {α : Type u_1} {x : α} {e e' : Sym2 α} (he : x ∈ e) (he' : x ∉ e') : e ≠ e'

Two unordered pairs differ if an element belongs to one but not the other.