English
UV-compression is injective on the domain restricted to those elements not already compressed into the ground set.
Русский
UV-компрессия инъективна на области, состоящей из элементов, не превращённых в другой элемент набора.
LaTeX
$$$\\mathrm{Set.InjOn} (\\lambda x,\\mathrm{compress}\\ u\\ v\\ x)\\; \\text{on} \\; {a \\in s \\mid \\mathrm{compress}\\ u v a \\notin s}$$$
Lean4
/-- UV-compressing `a` means removing `v` from it and adding `u` if `a` and `u` are disjoint and
`v ≤ a` (it replaces the `v` part of `a` by the `u` part). Else, UV-compressing `a` doesn't do
anything. This is most useful when `u` and `v` are disjoint finsets of the same size. -/
def compress (u v a : α) : α :=
if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a
