Theorems · Theorem · combinatorics

sup_sdiff_injOn

∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (u v : α),
  Set.InjOn (fun x => (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}

UV-compression is injective on the elements it moves. See UV.compress.

Defined in

Mathlib.Combinatorics.SetFamily.Compression.UV

Cited by

1 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GeneralizedBooleanAlgebra