Theorems · Theorem · combinatorics

UV.disjoint_of_mem_compression_of_notMem

∀ {α : 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 → Disjoint v a

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: GeneralizedBooleanAlgebra DecidableRel DecidableLE DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement and proof · cited by 13,712
Disjointstatement and proof · cited by 2,201
GeneralizedBooleanAlgebrastatement and proof · cited by 204
disjoint_sdiff_self_rightproof · cited by 22
UV.compressproof · cited by 20
UV.compressionstatement and proof · cited by 15
UV.mem_compressionproof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.

UV.shadow_compression_subset_compression_shadowproof · cited by 1