card_shadow_compression_le — Mathlib

English

The size of the shadow does not increase under UV-compression: card(∂(𝓒 u v 𝒜)) ≤ card(∂ 𝒜).

Русский

Размер тени не увеличивается после UV-сжатия: |∂(𝓒_{u,v} 𝒜)| ≤ |∂𝒜|.

LaTeX

$$$\\#\\partial(\\mathcal{C}_{u,v} \\mathcal{A}) \\le \\#(\\partial \\mathcal{A})$$$

Lean4

/-- 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 UV-compression fact needed for
Kruskal-Katona. -/
theorem card_shadow_compression_le (u v : Finset α) (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) :
    #(∂ (𝓒 u v 𝒜)) ≤ #(∂ 𝒜) :=
  (card_le_card <| shadow_compression_subset_compression_shadow _ _ huv).trans (card_compression _ _ _).le

Похожие утверждения