Theorems · Theorem · combinatorics

UV.mem_of_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 → v ≤ a → (v = ⊥ → u = ⊥) → a ∈ s

If a is in the u, v-compression but v ≤ a, then a must have been in the original family.

Defined in

Mathlib.Combinatorics.SetFamily.Compression.UV

Cited by

1 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraDecidableRelDecidableLEDecidableEq