compression_self — Mathlib

English

For any u and finite s, compressing with identical u and v yields the original finite set: 𝓒 u u s = s.

Русский

Для любых u и конечного s сжатие с идентичными параметрами возвращает исходный набор: 𝓒_{u,u}(s) = s.

LaTeX

$$$\\mathcal{C}_{u,u}(s) = s$$$

Lean4

@[simp]
theorem compression_self (u : α) (s : Finset α) : 𝓒 u u s = s :=
  by
  unfold compression
  convert union_empty s
  · ext a
    rw [mem_filter, compress_self, and_self_iff]
  · refine eq_empty_of_forall_notMem fun a ha ↦ ?_
    simp_rw [mem_filter, mem_image, compress_self] at ha
    obtain ⟨⟨b, hb, rfl⟩, hb'⟩ := ha
    exact hb' hb

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