compression_idem — Mathlib

English

Compressing twice yields the same result as compressing once: 𝓒 u v (𝓒 u v s) = 𝓒 u v s.

Русский

Сжатие дважды равно одному разу: 𝓒_{u,v}(𝓒_{u,v}(s)) = 𝓒_{u,v}(s).

LaTeX

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

Lean4

/-- Compressing a family is idempotent. -/
@[simp]
theorem compression_idem (u v : α) (s : Finset α) : 𝓒 u v (𝓒 u v s) = 𝓒 u v s :=
  by
  have h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅ :=
    filter_false_of_mem fun a ha h ↦ h <| compress_mem_compression_of_mem_compression ha
  rw [compression, filter_image, h, image_empty, ← h]
  exact filter_union_filter_neg_eq _ (compression u v s)

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