card_compression — Mathlib

English

Compression preserves size: the number of elements remains unchanged after compression: |𝓒 u v s| = |s|.

Русский

Сжатие сохраняет размер: после сжатия количество элементов не меняется: |𝓒_{u,v}(s)| = |s|.

LaTeX

$$#(|𝓒_{u,v}(s)| = |s|)$$

Lean4

/-- Compressing a family doesn't change its size. -/
@[simp]
theorem card_compression (u v : α) (s : Finset α) : #(𝓒 u v s) = #s := by
  rw [compression, card_union_of_disjoint compress_disjoint, filter_image, card_image_of_injOn compress_injOn, ←
    card_union_of_disjoint (disjoint_filter_filter_neg s _ _), filter_union_filter_neg_eq]

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