Theorems · Theorem · combinatorics

UV.mem_compression

∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α],
  a ∈ UV.compression u v s ↔ a ∈ s ∧ UV.compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, UV.compress u v b = a

a is in the UV-compressed family iff it's in the original and its compression is in the original, or it's not in the original but it's the compression of something in the original.

Defined in

Mathlib.Combinatorics.SetFamily.Compression.UV

Cited by

9 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraDecidableRelDecidableLEDecidableEq