Theorems · Theorem · combinatorics

UV.compress_mem_compression

∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ s → UV.compress u v a ∈ UV.compression u v s

Defined in

Mathlib.Combinatorics.SetFamily.Compression.UV

Cited by

0 results in Mathlib

Foundations

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

Assumes

GeneralizedBooleanAlgebraDecidableRelDecidableLEDecidableEq