Theorems · Definition · combinatorics

UV.compression

{α : Type u_1} →
  [inst : GeneralizedBooleanAlgebra α] →
    [DecidableRel Disjoint] → [DecidableLE α] → [DecidableEq α] → α → α → Finset α → Finset α

To UV-compress a set family, we compress each of its elements, except that we don't want to reduce the cardinality, so we keep all elements whose compression is already present.

Defined in

Mathlib.Combinatorics.SetFamily.Compression.UV

Cited by

15 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraDecidableRelDecidableLEDecidableEq