Theorems · Theorem · combinatorics

UV.shadow_compression_subset_compression_shadow

∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} (u v : Finset α),
  (∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) →
    (UV.compression u v 𝒜).shadow ⊆ UV.compression u v 𝒜.shadow

UV-compression reduces the size of the shadow of 𝒜 if, for all x ∈ u there is y ∈ v such that 𝒜 is (u.erase x, v.erase y)-compressed. This is the key fact about compression for Kruskal-Katona.

Defined in

Mathlib.Combinatorics.SetFamily.Compression.UV

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq