English
UV-compression is injective on the set of non-compressed elements of the ground set.
Русский
UV-компрессия инъективна на множестве элементов, не сжатых ранее.
LaTeX
$$$\\text{UV.compress\\_injOn}: \\mathrm{Set.InjOn} (\\mathrm{compress}\\ u v) \\; (\\text{Finset.filter}(\\text{fun } a \\mapsto \\lnot a \\in s) ).$$$
Lean4
/-- UV-compression is injective on the sets that are not UV-compressed. -/
theorem compress_injOn : Set.InjOn (compress u v) ↑({a ∈ s | compress u v a ∉ s}) :=
by
intro a ha b hb hab
rw [mem_coe, mem_filter] at ha hb
rw [compress] at ha hab
split_ifs at ha hab with has
· rw [compress] at hb hab
split_ifs at hb hab with hbs
· exact sup_sdiff_injOn u v has hbs hab
· exact (hb.2 hb.1).elim
· exact (ha.2 ha.1).elim
