card_compress — Mathlib

English

If the two finite sets u and v have the same size, and A is a finite family of finite sets with a given size r, then the compressed family has the same size r.

Русский

Если #u = #v и 𝒜 — конечное множество финитных множеств размерности r, то 𝓒 u v 𝒜 имеет размер r.

LaTeX

$$\\#(\\mathcal{C}_{u,v} 𝒜) = \\#𝒜$$

Lean4

/-- Compressing a finset doesn't change its size. -/
theorem card_compress (huv : #u = #v) (a : Finset α) : #(compress u v a) = #a :=
  by
  unfold compress
  split_ifs with h
  ·
    rw [card_sdiff_of_subset (h.2.trans le_sup_left), sup_eq_union, card_union_of_disjoint h.1.symm, huv,
      add_tsub_cancel_right]
  · rfl

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