English
UV-supersymmetric compression is injective on the set of x such that Disjoint u x and v ≤ x, under the map x ↦ x ⊔ u \\ v.
Русский
UV-компрессия инъективна на множестве x с условиями Disjoint u x и v ≤ x под отображением x ↦ (x ⊔ u) \\ v.
LaTeX
$$$\\{x \\mid Disjoint\\ u\\ x \\land v \\le x\\}.InjOn\\bigl(x \\mapsto (x \\lor u) \\setminus v\\bigr)$$$
Lean4
/-- UV-compression is injective on the elements it moves. See `UV.compress`. -/
theorem sup_sdiff_injOn [GeneralizedBooleanAlgebra α] (u v : α) :
{x | Disjoint u x ∧ v ≤ x}.InjOn fun x => (x ⊔ u) \ v :=
by
rintro a ha b hb hab
have h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v :=
by
dsimp at hab
rw [hab]
rwa [sdiff_sdiff_comm, ha.1.symm.sup_sdiff_cancel_right, sdiff_sdiff_comm, hb.1.symm.sup_sdiff_cancel_right,
sdiff_sup_cancel ha.2, sdiff_sup_cancel hb.2] at h
